aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/ExtrHaskellString.v20
-rw-r--r--plugins/extraction/ExtrOcamlString.v16
-rw-r--r--plugins/extraction/big.ml24
-rw-r--r--plugins/extraction/common.ml2
-rw-r--r--plugins/extraction/extract_env.ml17
-rw-r--r--plugins/extraction/extract_env.mli2
-rw-r--r--plugins/extraction/extraction.ml142
-rw-r--r--plugins/extraction/g_extraction.mlg (renamed from plugins/extraction/g_extraction.ml4)83
-rw-r--r--plugins/extraction/haskell.ml2
-rw-r--r--plugins/extraction/json.ml4
-rw-r--r--plugins/extraction/miniml.ml1
-rw-r--r--plugins/extraction/miniml.mli1
-rw-r--r--plugins/extraction/mlutil.ml29
-rw-r--r--plugins/extraction/modutil.ml2
-rw-r--r--plugins/extraction/ocaml.ml4
-rw-r--r--plugins/extraction/scheme.ml2
-rw-r--r--plugins/extraction/table.ml92
17 files changed, 284 insertions, 159 deletions
diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v
index a4a40d3c5a..8c61f4e96b 100644
--- a/plugins/extraction/ExtrHaskellString.v
+++ b/plugins/extraction/ExtrHaskellString.v
@@ -6,6 +6,7 @@ Require Coq.extraction.Extraction.
Require Import Ascii.
Require Import String.
+Require Import Coq.Strings.Byte.
(**
* At the moment, Coq's extraction has no way to add extra import
@@ -40,3 +41,22 @@ Extract Inlined Constant Ascii.eqb => "(Prelude.==)".
Extract Inductive string => "Prelude.String" [ "([])" "(:)" ].
Extract Inlined Constant String.string_dec => "(Prelude.==)".
Extract Inlined Constant String.eqb => "(Prelude.==)".
+
+(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *)
+Extract Inductive byte => "Prelude.Char"
+["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"].
+
+Extract Inlined Constant Byte.eqb => "(Prelude.==)".
+Extract Inlined Constant Byte.byte_eq_dec => "(Prelude.==)".
+Extract Inlined Constant Ascii.ascii_of_byte => "(\x -> x)".
+Extract Inlined Constant Ascii.byte_of_ascii => "(\x -> x)".
+
+(*
+Require Import ExtrHaskellBasic.
+Definition test := "ceci est un test"%string.
+Definition test2 := List.map (option_map Byte.to_nat) (List.map Byte.of_nat (List.seq 0 256)).
+Definition test3 := List.map ascii_of_nat (List.seq 0 256).
+
+Extraction Language Haskell.
+Recursive Extraction test Ascii.zero Ascii.one test2 test3 byte_rect.
+*)
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
index a2a6a8fe67..f094d4860e 100644
--- a/plugins/extraction/ExtrOcamlString.v
+++ b/plugins/extraction/ExtrOcamlString.v
@@ -12,7 +12,7 @@
Require Coq.extraction.Extraction.
-Require Import Ascii String.
+Require Import Ascii String Coq.Strings.Byte.
Extract Inductive ascii => char
[
@@ -37,7 +37,19 @@ Extract Inlined Constant Ascii.eqb => "(=)".
Extract Inductive string => "char list" [ "[]" "(::)" ].
+(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *)
+Extract Inductive byte => char
+["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"].
+
+Extract Inlined Constant Byte.eqb => "(=)".
+Extract Inlined Constant Byte.byte_eq_dec => "(=)".
+Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)".
+Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)".
+
(*
Definition test := "ceci est un test"%string.
-Recursive Extraction test Ascii.zero Ascii.one.
+Definition test2 := List.map (option_map Byte.to_nat) (List.map Byte.of_nat (List.seq 0 256)).
+Definition test3 := List.map ascii_of_nat (List.seq 0 256).
+
+Recursive Extraction test Ascii.zero Ascii.one test2 test3 byte_rect.
*)
diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml
index 9c0f373c6a..c675eacc92 100644
--- a/plugins/extraction/big.ml
+++ b/plugins/extraction/big.ml
@@ -20,8 +20,10 @@ type big_int = Big_int.big_int
let zero = zero_big_int
(** The big integer [0]. *)
+
let one = unit_big_int
(** The big integer [1]. *)
+
let two = big_int_of_int 2
(** The big integer [2]. *)
@@ -29,28 +31,39 @@ let two = big_int_of_int 2
let opp = minus_big_int
(** Unary negation. *)
+
let abs = abs_big_int
(** Absolute value. *)
+
let add = add_big_int
(** Addition. *)
+
let succ = succ_big_int
(** Successor (add 1). *)
+
let add_int = add_int_big_int
(** Addition of a small integer to a big integer. *)
+
let sub = sub_big_int
(** Subtraction. *)
+
let pred = pred_big_int
(** Predecessor (subtract 1). *)
+
let mult = mult_big_int
(** Multiplication of two big integers. *)
+
let mult_int = mult_int_big_int
(** Multiplication of a big integer by a small integer *)
+
let square = square_big_int
(** Return the square of the given big integer *)
+
let sqrt = sqrt_big_int
(** [sqrt_big_int a] returns the integer square root of [a],
that is, the largest big integer [r] such that [r * r <= a].
Raise [Invalid_argument] if [a] is negative. *)
+
let quomod = quomod_big_int
(** Euclidean division of two big integers.
The first part of the result is the quotient,
@@ -58,14 +71,18 @@ let quomod = quomod_big_int
Writing [(q,r) = quomod_big_int a b], we have
[a = q * b + r] and [0 <= r < |b|].
Raise [Division_by_zero] if the divisor is zero. *)
+
let div = div_big_int
(** Euclidean quotient of two big integers.
This is the first result [q] of [quomod_big_int] (see above). *)
+
let modulo = mod_big_int
(** Euclidean modulus of two big integers.
This is the second result [r] of [quomod_big_int] (see above). *)
+
let gcd = gcd_big_int
(** Greatest common divisor of two big integers. *)
+
let power = power_big_int_positive_big_int
(** Exponentiation functions. Return the big integer
representing the first argument [a] raised to the power [b]
@@ -78,18 +95,22 @@ let power = power_big_int_positive_big_int
let sign = sign_big_int
(** Return [0] if the given big integer is zero,
[1] if it is positive, and [-1] if it is negative. *)
+
let compare = compare_big_int
(** [compare_big_int a b] returns [0] if [a] and [b] are equal,
[1] if [a] is greater than [b], and [-1] if [a] is smaller
than [b]. *)
+
let eq = eq_big_int
let le = le_big_int
let ge = ge_big_int
let lt = lt_big_int
let gt = gt_big_int
(** Usual boolean comparisons between two big integers. *)
+
let max = max_big_int
(** Return the greater of its two arguments. *)
+
let min = min_big_int
(** Return the smaller of its two arguments. *)
@@ -98,6 +119,7 @@ let min = min_big_int
let to_string = string_of_big_int
(** Return the string representation of the given big integer,
in decimal (base 10). *)
+
let of_string = big_int_of_string
(** Convert a string to a big integer, in decimal.
The string consists of an optional [-] or [+] sign,
@@ -107,6 +129,7 @@ let of_string = big_int_of_string
let of_int = big_int_of_int
(** Convert a small integer to a big integer. *)
+
let is_int = is_int_big_int
(** Test whether the given big integer is small enough to
be representable as a small integer (type [int])
@@ -115,6 +138,7 @@ let is_int = is_int_big_int
[a] is between 2{^30} and 2{^30}-1. On a 64-bit platform,
[is_int_big_int a] returns [true] if and only if
[a] is between -2{^62} and 2{^62}-1. *)
+
let to_int = int_of_big_int
(** Convert a big integer to a small integer (type [int]).
Raises [Failure "int_of_big_int"] if the big integer
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index bdeb6fca60..59c57cc544 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -125,7 +125,7 @@ module KOrd =
struct
type t = kind * string
let compare (k1, s1) (k2, s2) =
- let c = Pervasives.compare k1 k2 (** OK *) in
+ let c = Pervasives.compare k1 k2 (* OK *) in
if c = 0 then String.compare s1 s2
else c
end
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index b0f6301192..8f17f7b2dd 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -147,10 +147,10 @@ let check_fix env sg cb i =
| Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd)
| CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd)
| _ -> raise Impossible)
- | Undef _ | OpaqueDef _ -> raise Impossible
+ | Undef _ | OpaqueDef _ | Primitive _ -> raise Impossible
let prec_declaration_equal sg (na1, ca1, ta1) (na2, ca2, ta2) =
- Array.equal Name.equal na1 na2 &&
+ Array.equal (Context.eq_annot Name.equal) na1 na2 &&
Array.equal (EConstr.eq_constr sg) ca1 ca2 &&
Array.equal (EConstr.eq_constr sg) ta1 ta2
@@ -750,16 +750,19 @@ let extract_and_compile l =
Feedback.msg_notice (str "Extracted code successfully compiled")
(* Show the extraction of the current ongoing proof *)
-
-let show_extraction () =
+let show_extraction ~pstate =
+ let pstate = match pstate with
+ | None -> CErrors.user_err Pp.(str "No ongoing proof")
+ | Some pstate -> pstate
+ in
init ~inner:true false false;
- let prf = Proof_global.give_me_the_proof () in
- let sigma, env = Pfedit.get_current_context () in
+ let prf = Proof_global.give_me_the_proof pstate in
+ let sigma, env = Pfedit.get_current_context pstate in
let trms = Proof.partial_proof prf in
let extr_term t =
let ast, ty = extract_constr env sigma t in
let mp = Lib.current_mp () in
- let l = Label.of_id (Proof_global.get_current_proof_name ()) in
+ let l = Label.of_id (Proof_global.get_current_proof_name pstate) in
let fake_ref = ConstRef (Constant.make2 mp l) in
let decl = Dterm (fake_ref, ast, ty) in
print_one_decl [] mp decl
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 54fde2ca46..7ba7e05019 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -40,4 +40,4 @@ val structure_for_compute :
(* Show the extraction of the current ongoing proof *)
-val show_extraction : unit -> unit
+val show_extraction : pstate:Proof_global.t option -> unit
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 67c605ea1d..c9cfd74362 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -13,6 +13,7 @@ open Util
open Names
open Term
open Constr
+open Context
open Declarations
open Declareops
open Environ
@@ -73,13 +74,18 @@ type flag = info * scheme
(*s [flag_of_type] transforms a type [t] into a [flag].
Really important function. *)
+let info_of_family = function
+ | InSProp | InProp -> Logic
+ | InSet | InType -> Info
+
+let info_of_sort s = info_of_family (Sorts.family s)
+
let rec flag_of_type env sg t : flag =
let t = whd_all env sg t in
match EConstr.kind sg t with
| Prod (x,t,c) -> flag_of_type (EConstr.push_rel (LocalAssum (x,t)) env) sg c
- | Sort s when Sorts.is_prop (EConstr.ESorts.kind sg s) -> (Logic,TypeScheme)
- | Sort _ -> (Info,TypeScheme)
- | _ -> if (sort_of env sg t) == InProp then (Logic,Default) else (Info,Default)
+ | Sort s -> (info_of_sort (EConstr.ESorts.kind sg s),TypeScheme)
+ | _ -> (info_of_family (sort_of env sg t),Default)
(*s Two particular cases of [flag_of_type]. *)
@@ -179,7 +185,7 @@ let rec type_sign_vl env sg c =
| Prod (n,t,d) ->
let s,vl = type_sign_vl (push_rel_assum (n,t) env) sg d in
if not (is_info_scheme env sg t) then Kill Kprop::s, vl
- else Keep::s, (make_typvar n vl) :: vl
+ else Keep::s, (make_typvar n.binder_name vl) :: vl
| _ -> [],[]
let rec nb_default_params env sg c =
@@ -259,14 +265,14 @@ let rec extract_type env sg db j c args =
(* We just accumulate the arguments. *)
extract_type env sg db j d (Array.to_list args' @ args)
| Lambda (_,_,d) ->
- (match args with
+ (match args with
| [] -> assert false (* A lambda cannot be a type. *)
| a :: args -> extract_type env sg db j (EConstr.Vars.subst1 a d) args)
| Prod (n,t,d) ->
- assert (List.is_empty args);
- let env' = push_rel_assum (n,t) env in
+ assert (List.is_empty args);
+ let env' = push_rel_assum (n,t) env in
(match flag_of_type env sg t with
- | (Info, Default) ->
+ | (Info, Default) ->
(* Standard case: two [extract_type] ... *)
let mld = extract_type env' sg (0::db) j d [] in
(match expand env mld with
@@ -291,7 +297,7 @@ let rec extract_type env sg db j c args =
(match EConstr.lookup_rel n env with
| LocalDef (_,t,_) ->
extract_type env sg db j (EConstr.Vars.lift n t) args
- | _ ->
+ | _ ->
(* Asks [db] a translation for [n]. *)
if n > List.length db then Tunknown
else let n' = List.nth db (n-1) in
@@ -304,9 +310,9 @@ let rec extract_type env sg db j c args =
| (Info, TypeScheme) ->
let mlt = extract_type_app env sg db (r, type_sign env sg typ) args in
(match (lookup_constant kn env).const_body with
- | Undef _ | OpaqueDef _ -> mlt
- | Def _ when is_custom (ConstRef kn) -> mlt
- | Def lbody ->
+ | Undef _ | OpaqueDef _ | Primitive _ -> mlt
+ | Def _ when is_custom (ConstRef kn) -> mlt
+ | Def lbody ->
let newc = applistc (get_body lbody) args in
let mlt' = extract_type env sg db j newc [] in
(* ML type abbreviations interact badly with Coq *)
@@ -318,7 +324,7 @@ let rec extract_type env sg db j c args =
| (Info, Default) ->
(* Not an ML type, for example [(c:forall X, X->X) Type nat] *)
(match (lookup_constant kn env).const_body with
- | Undef _ | OpaqueDef _ -> Tunknown (* Brutal approx ... *)
+ | Undef _ | OpaqueDef _ | Primitive _ -> Tunknown (* Brutal approx ... *)
| Def lbody ->
(* We try to reduce. *)
let newc = applistc (get_body lbody) args in
@@ -346,7 +352,7 @@ let rec extract_type env sg db j c args =
| (Info, TypeScheme) ->
extract_type_app env sg db (r, type_sign env sg ty) args
| (Info, Default) -> Tunknown))
- | Cast _ | LetIn _ | Construct _ -> assert false
+ | Cast _ | LetIn _ | Construct _ | Int _ -> assert false
(*s Auxiliary function dealing with type application.
Precondition: [r] is a type scheme represented by the signature [s],
@@ -492,8 +498,8 @@ and extract_really_ind env kn mib =
(* Now we're sure it's a record. *)
(* First, we find its field names. *)
let rec names_prod t = match Constr.kind t with
- | Prod(n,_,t) -> n::(names_prod t)
- | LetIn(_,_,_,t) -> names_prod t
+ | Prod(n,_,t) -> n::(names_prod t)
+ | LetIn(_,_,_,t) -> names_prod t
| Cast(t,_,_) -> names_prod t
| _ -> []
in
@@ -506,9 +512,9 @@ and extract_really_ind env kn mib =
| [],[] -> []
| _::l, typ::typs when isTdummy (expand env typ) ->
select_fields l typs
- | Anonymous::l, typ::typs ->
+ | {binder_name=Anonymous}::l, typ::typs ->
None :: (select_fields l typs)
- | Name id::l, typ::typs ->
+ | {binder_name=Name id}::l, typ::typs ->
let knp = Constant.make2 mp (Label.of_id id) in
(* Is it safe to use [id] for projections [foo.id] ? *)
if List.for_all ((==) Keep) (type2signature env typ)
@@ -551,8 +557,8 @@ and extract_really_ind env kn mib =
and extract_type_cons env sg db dbmap c i =
match EConstr.kind sg (whd_all env sg c) with
| Prod (n,t,d) ->
- let env' = push_rel_assum (n,t) env in
- let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in
+ let env' = push_rel_assum (n,t) env in
+ let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in
let l = extract_type_cons env' sg db' dbmap d (i+1) in
(extract_type env sg db 0 t []) :: l
| _ -> []
@@ -564,7 +570,7 @@ and mlt_env env r = match r with
| ConstRef kn ->
let cb = Environ.lookup_constant kn env in
match cb.const_body with
- | Undef _ | OpaqueDef _ -> None
+ | Undef _ | OpaqueDef _ | Primitive _ -> None
| Def l_body ->
match lookup_typedef kn cb with
| Some _ as o -> o
@@ -615,17 +621,18 @@ let rec extract_term env sg mle mlt c args =
| App (f,a) ->
extract_term env sg mle mlt f (Array.to_list a @ args)
| Lambda (n, t, d) ->
- let id = id_of_name n in
+ let id = map_annot id_of_name n in
+ let idna = map_annot Name.mk_name id in
(match args with
| a :: l ->
(* We make as many [LetIn] as possible. *)
let l' = List.map (EConstr.Vars.lift 1) l in
- let d' = EConstr.mkLetIn (Name id,a,t,applistc d l') in
+ let d' = EConstr.mkLetIn (idna,a,t,applistc d l') in
extract_term env sg mle mlt d' []
- | [] ->
- let env' = push_rel_assum (Name id, t) env in
+ | [] ->
+ let env' = push_rel_assum (idna, t) env in
let id, a =
- try check_default env sg t; Id id, new_meta()
+ try check_default env sg t; Id id.binder_name, new_meta()
with NotDefault d -> Dummy, Tdummy d
in
let b = new_meta () in
@@ -634,9 +641,9 @@ let rec extract_term env sg mle mlt c args =
let d' = extract_term env' sg (Mlenv.push_type mle a) b d [] in
put_magic_if magic (MLlam (id, d')))
| LetIn (n, c1, t1, c2) ->
- let id = id_of_name n in
- let env' = EConstr.push_rel (LocalDef (Name id, c1, t1)) env in
- (* We directly push the args inside the [LetIn].
+ let id = map_annot id_of_name n in
+ let env' = EConstr.push_rel (LocalDef (map_annot Name.mk_name id, c1, t1)) env in
+ (* We directly push the args inside the [LetIn].
TODO: the opt_let_app flag is supposed to prevent that *)
let args' = List.map (EConstr.Vars.lift 1) args in
(try
@@ -649,7 +656,7 @@ let rec extract_term env sg mle mlt c args =
then Mlenv.push_gen mle a
else Mlenv.push_type mle a
in
- MLletin (Id id, c1', extract_term env' sg mle' mlt c2 args')
+ MLletin (Id id.binder_name, c1', extract_term env' sg mle' mlt c2 args')
with NotDefault d ->
let mle' = Mlenv.push_std_type mle (Tdummy d) in
ast_pop (extract_term env' sg mle' mlt c2 args'))
@@ -683,6 +690,7 @@ let rec extract_term env sg mle mlt c args =
let vty = extract_type env sg [] 0 ty [] in
let extract_var mlt = put_magic (mlt,vty) (MLglob (VarRef v)) in
extract_app env sg mle mlt extract_var args
+ | Int i -> assert (args = []); MLuint i
| Ind _ | Prod _ | Sort _ -> assert false
(*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
@@ -912,7 +920,7 @@ and extract_fix env sg mle i (fi,ti,ci as recd) mlt =
metas.(i) <- mlt;
let mle = Array.fold_left Mlenv.push_type mle metas in
let ei = Array.map2 (extract_maybe_term env sg mle) metas ci in
- MLfix (i, Array.map id_of_name fi, ei)
+ MLfix (i, Array.map (fun x -> id_of_name x.binder_name) fi, ei)
(*S ML declarations. *)
@@ -988,7 +996,7 @@ let extract_std_constant env sg kn body typ =
(* The initial ML environment. *)
let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in
(* The lambdas names. *)
- let ids = List.map (fun (n,_) -> Id (id_of_name n)) rels in
+ let ids = List.map (fun (n,_) -> Id (id_of_name n.binder_name)) rels in
(* The according Coq environment. *)
let env = push_rels_assum rels env in
(* The real extraction: *)
@@ -1031,6 +1039,60 @@ let extract_fixpoint env sg vkn (fi,ti,ci) =
current_fixpoints := [];
Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types)
+(** Because of automatic unboxing the easy way [mk_def c] on the
+ constant body of primitive projections doesn't work. We pretend
+ that they are implemented by matches until someone figures out how
+ to clean it up (test with #4710 when working on this). *)
+let fake_match_projection env p =
+ let ind = Projection.Repr.inductive p in
+ let proj_arg = Projection.Repr.arg p in
+ let mib, mip = Inductive.lookup_mind_specif env ind in
+ let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
+ let indu = mkIndU (ind,u) in
+ let ctx, paramslet =
+ let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in
+ let (ctx, cty) = mip.mind_nf_lc.(0) in
+ let cty = Term.it_mkProd_or_LetIn cty ctx in
+ let rctx, _ = decompose_prod_assum (Vars.substl subst cty) in
+ List.chop mip.mind_consnrealdecls.(0) rctx
+ in
+ let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
+ let ci = {
+ ci_ind = ind;
+ ci_npar = mib.mind_nparams;
+ ci_cstr_ndecls = mip.mind_consnrealdecls;
+ ci_cstr_nargs = mip.mind_consnrealargs;
+ ci_relevance = Declareops.relevance_of_projection_repr mib p;
+ ci_pp_info;
+ }
+ in
+ let x = match mib.mind_record with
+ | NotRecord | FakeRecord -> assert false
+ | PrimRecord info ->
+ let x, _, _, _ = info.(snd ind) in
+ make_annot (Name x) mip.mind_relevance
+ in
+ let indty = mkApp (indu, Context.Rel.to_extended_vect mkRel 0 paramslet) in
+ let rec fold arg j subst = function
+ | [] -> assert false
+ | LocalAssum (na,ty) :: rem ->
+ let ty = Vars.substl subst (liftn 1 j ty) in
+ if arg != proj_arg then
+ let lab = match na.binder_name with Name id -> Label.of_id id | Anonymous -> assert false in
+ let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in
+ fold (arg+1) (j+1) (mkProj (Projection.make kn false, mkRel 1)::subst) rem
+ else
+ let p = mkLambda (x, lift 1 indty, liftn 1 2 ty) in
+ let branch = lift 1 (it_mkLambda_or_LetIn (mkRel (List.length ctx - (j-1))) ctx) in
+ let body = mkCase (ci, p, mkRel 1, [|branch|]) in
+ it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt
+ | LocalDef (_,c,t) :: rem ->
+ let c = liftn 1 j c in
+ let c1 = Vars.substl subst c in
+ fold arg (j+1) (c1::subst) rem
+ in
+ fold 0 1 [] (List.rev ctx)
+
let extract_constant env kn cb =
let sg = Evd.from_env env in
let r = ConstRef kn in
@@ -1063,15 +1125,12 @@ let extract_constant env kn cb =
| (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop)
| (Info,TypeScheme) ->
(match cb.const_body with
- | Undef _ -> warn_info (); mk_typ_ax ()
+ | Primitive _ | Undef _ -> warn_info (); mk_typ_ax ()
| Def c ->
(match Recordops.find_primitive_projection kn with
| None -> mk_typ (get_body c)
| Some p ->
- let p = Projection.make p false in
- let ind = Projection.inductive p in
- let bodies = Inductiveops.legacy_match_projection env ind in
- let body = bodies.(Projection.arg p) in
+ let body = fake_match_projection env p in
mk_typ (EConstr.of_constr body))
| OpaqueDef c ->
add_opaque r;
@@ -1079,15 +1138,12 @@ let extract_constant env kn cb =
else mk_typ_ax ())
| (Info,Default) ->
(match cb.const_body with
- | Undef _ -> warn_info (); mk_ax ()
+ | Primitive _ | Undef _ -> warn_info (); mk_ax ()
| Def c ->
(match Recordops.find_primitive_projection kn with
| None -> mk_def (get_body c)
| Some p ->
- let p = Projection.make p false in
- let ind = Projection.inductive p in
- let bodies = Inductiveops.legacy_match_projection env ind in
- let body = bodies.(Projection.arg p) in
+ let body = fake_match_projection env p in
mk_def (EConstr.of_constr body))
| OpaqueDef c ->
add_opaque r;
@@ -1107,7 +1163,7 @@ let extract_constant_spec env kn cb =
| (Info, TypeScheme) ->
let s,vl = type_sign_vl env sg typ in
(match cb.const_body with
- | Undef _ | OpaqueDef _ -> Stype (r, vl, None)
+ | Undef _ | OpaqueDef _ | Primitive _ -> Stype (r, vl, None)
| Def body ->
let db = db_from_sign s in
let body = get_body body in
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.mlg
index 93909f3e64..d7bb27f121 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.mlg
@@ -8,14 +8,19 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+{
+
open Pcoq.Prim
+}
+
DECLARE PLUGIN "extraction_plugin"
+{
+
(* ML names *)
open Ltac_plugin
-open Genarg
open Stdarg
open Pp
open Names
@@ -24,23 +29,31 @@ open Extract_env
let pr_mlname _ _ _ s = spc () ++ qs s
+}
+
ARGUMENT EXTEND mlname
TYPED AS string
- PRINTED BY pr_mlname
-| [ preident(id) ] -> [ id ]
-| [ string(s) ] -> [ s ]
+ PRINTED BY { pr_mlname }
+| [ preident(id) ] -> { id }
+| [ string(s) ] -> { s }
END
+{
+
let pr_int_or_id _ _ _ = function
| ArgInt i -> int i
| ArgId id -> Id.print id
+}
+
ARGUMENT EXTEND int_or_id
- PRINTED BY pr_int_or_id
-| [ preident(id) ] -> [ ArgId (Id.of_string id) ]
-| [ integer(i) ] -> [ ArgInt i ]
+ PRINTED BY { pr_int_or_id }
+| [ preident(id) ] -> { ArgId (Id.of_string id) }
+| [ integer(i) ] -> { ArgInt i }
END
+{
+
let pr_language = function
| Ocaml -> str "OCaml"
| Haskell -> str "Haskell"
@@ -52,117 +65,119 @@ let warn_deprecated_ocaml_spelling =
(fun () ->
strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\"."))
+}
+
VERNAC ARGUMENT EXTEND language
-PRINTED BY pr_language
-| [ "Ocaml" ] -> [ let _ = warn_deprecated_ocaml_spelling () in Ocaml ]
-| [ "OCaml" ] -> [ Ocaml ]
-| [ "Haskell" ] -> [ Haskell ]
-| [ "Scheme" ] -> [ Scheme ]
-| [ "JSON" ] -> [ JSON ]
+PRINTED BY { pr_language }
+| [ "Ocaml" ] -> { let _ = warn_deprecated_ocaml_spelling () in Ocaml }
+| [ "OCaml" ] -> { Ocaml }
+| [ "Haskell" ] -> { Haskell }
+| [ "Scheme" ] -> { Scheme }
+| [ "JSON" ] -> { JSON }
END
(* Extraction commands *)
VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY
(* Extraction in the Coq toplevel *)
-| [ "Extraction" global(x) ] -> [ simple_extraction x ]
-| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ full_extraction None l ]
+| [ "Extraction" global(x) ] -> { simple_extraction x }
+| [ "Recursive" "Extraction" ne_global_list(l) ] -> { full_extraction None l }
(* Monolithic extraction to a file *)
| [ "Extraction" string(f) ne_global_list(l) ]
- -> [ full_extraction (Some f) l ]
+ -> { full_extraction (Some f) l }
(* Extraction to a temporary file and OCaml compilation *)
| [ "Extraction" "TestCompile" ne_global_list(l) ]
- -> [ extract_and_compile l ]
+ -> { extract_and_compile l }
END
VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY
(* Same, with content splitted in several files *)
| [ "Separate" "Extraction" ne_global_list(l) ]
- -> [ separate_extraction l ]
+ -> { separate_extraction l }
END
(* Modular extraction (one Coq library = one ML module) *)
VERNAC COMMAND EXTEND ExtractionLibrary CLASSIFIED AS QUERY
| [ "Extraction" "Library" ident(m) ]
- -> [ extraction_library false m ]
+ -> { extraction_library false m }
END
VERNAC COMMAND EXTEND RecursiveExtractionLibrary CLASSIFIED AS QUERY
| [ "Recursive" "Extraction" "Library" ident(m) ]
- -> [ extraction_library true m ]
+ -> { extraction_library true m }
END
(* Target Language *)
VERNAC COMMAND EXTEND ExtractionLanguage CLASSIFIED AS SIDEFF
| [ "Extraction" "Language" language(l) ]
- -> [ extraction_language l ]
+ -> { extraction_language l }
END
VERNAC COMMAND EXTEND ExtractionInline CLASSIFIED AS SIDEFF
(* Custom inlining directives *)
| [ "Extraction" "Inline" ne_global_list(l) ]
- -> [ extraction_inline true l ]
+ -> { extraction_inline true l }
END
VERNAC COMMAND EXTEND ExtractionNoInline CLASSIFIED AS SIDEFF
| [ "Extraction" "NoInline" ne_global_list(l) ]
- -> [ extraction_inline false l ]
+ -> { extraction_inline false l }
END
VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY
| [ "Print" "Extraction" "Inline" ]
- -> [Feedback. msg_info (print_extraction_inline ()) ]
+ -> {Feedback. msg_info (print_extraction_inline ()) }
END
VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF
| [ "Reset" "Extraction" "Inline" ]
- -> [ reset_extraction_inline () ]
+ -> { reset_extraction_inline () }
END
VERNAC COMMAND EXTEND ExtractionImplicit CLASSIFIED AS SIDEFF
(* Custom implicit arguments of some csts/inds/constructors *)
| [ "Extraction" "Implicit" global(r) "[" int_or_id_list(l) "]" ]
- -> [ extraction_implicit r l ]
+ -> { extraction_implicit r l }
END
VERNAC COMMAND EXTEND ExtractionBlacklist CLASSIFIED AS SIDEFF
(* Force Extraction to not use some filenames *)
| [ "Extraction" "Blacklist" ne_ident_list(l) ]
- -> [ extraction_blacklist l ]
+ -> { extraction_blacklist l }
END
VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY
| [ "Print" "Extraction" "Blacklist" ]
- -> [ Feedback.msg_info (print_extraction_blacklist ()) ]
+ -> { Feedback.msg_info (print_extraction_blacklist ()) }
END
VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF
| [ "Reset" "Extraction" "Blacklist" ]
- -> [ reset_extraction_blacklist () ]
+ -> { reset_extraction_blacklist () }
END
(* Overriding of a Coq object by an ML one *)
VERNAC COMMAND EXTEND ExtractionConstant CLASSIFIED AS SIDEFF
| [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ]
- -> [ extract_constant_inline false x idl y ]
+ -> { extract_constant_inline false x idl y }
END
VERNAC COMMAND EXTEND ExtractionInlinedConstant CLASSIFIED AS SIDEFF
| [ "Extract" "Inlined" "Constant" global(x) "=>" mlname(y) ]
- -> [ extract_constant_inline true x [] y ]
+ -> { extract_constant_inline true x [] y }
END
VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF
| [ "Extract" "Inductive" global(x) "=>"
mlname(id) "[" mlname_list(idl) "]" string_opt(o) ]
- -> [ extract_inductive x id idl o ]
+ -> { extract_inductive x id idl o }
END
(* Show the extraction of the current proof *)
VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY
-| [ "Show" "Extraction" ]
- -> [ show_extraction () ]
+| ![ proof ] [ "Show" "Extraction" ]
+ -> { fun ~pstate -> let () = show_extraction ~pstate in pstate }
END
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 97fe9f24d5..a3cd92d556 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -214,6 +214,8 @@ let rec pp_expr par env args =
| MLmagic a ->
pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
| MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
+ | MLuint _ ->
+ pp_par par (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
and pp_cons_pat par r ppl =
pp_par par
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index e43c47d050..f88d29e9ed 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -155,6 +155,10 @@ let rec json_expr env = function
("value", json_expr env a)
]
| MLaxiom -> json_dict [("what", json_str "expr:axiom")]
+ | MLuint i -> json_dict [
+ ("what", json_str "expr:int");
+ ("int", json_str (Uint63.to_string i))
+ ]
and json_one_pat env (ids,p,t) =
let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in json_dict [
diff --git a/plugins/extraction/miniml.ml b/plugins/extraction/miniml.ml
index ce920ad6a0..b7f80d543b 100644
--- a/plugins/extraction/miniml.ml
+++ b/plugins/extraction/miniml.ml
@@ -126,6 +126,7 @@ and ml_ast =
| MLdummy of kill_reason
| MLaxiom
| MLmagic of ml_ast
+ | MLuint of Uint63.t
and ml_pattern =
| Pcons of GlobRef.t * ml_pattern list
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index ce920ad6a0..9df0f4964e 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -126,6 +126,7 @@ and ml_ast =
| MLdummy of kill_reason
| MLaxiom
| MLmagic of ml_ast
+ | MLuint of Uint63.t
and ml_pattern =
| Pcons of GlobRef.t * ml_pattern list
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 9f5c1f1a17..2432887673 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -66,7 +66,8 @@ let rec eq_ml_type t1 t2 = match t1, t2 with
| Tdummy k1, Tdummy k2 -> k1 == k2
| Tunknown, Tunknown -> true
| Taxiom, Taxiom -> true
-| _ -> false
+| (Tarr _ | Tglob _ | Tvar _ | Tvar' _ | Tmeta _ | Tdummy _ | Tunknown | Taxiom), _
+ -> false
and eq_ml_meta m1 m2 =
Int.equal m1.id m2.id && Option.equal eq_ml_type m1.contents m2.contents
@@ -107,7 +108,7 @@ let rec type_occurs alpha t =
| Tmeta {contents=Some u} -> type_occurs alpha u
| Tarr (t1, t2) -> type_occurs alpha t1 || type_occurs alpha t2
| Tglob (r,l) -> List.exists (type_occurs alpha) l
- | _ -> false
+ | (Tdummy _ | Tvar _ | Tvar' _ | Taxiom | Tunknown) -> false
(*s Most General Unificator *)
@@ -310,7 +311,7 @@ let isMLdummy = function MLdummy _ -> true | _ -> false
let sign_of_id = function
| Dummy -> Kill Kprop
- | _ -> Keep
+ | (Id _ | Tmp _) -> Keep
(* Classification of signatures *)
@@ -370,7 +371,10 @@ let eq_ml_ident i1 i2 = match i1, i2 with
| Dummy, Dummy -> true
| Id id1, Id id2 -> Id.equal id1 id2
| Tmp id1, Tmp id2 -> Id.equal id1 id2
-| _ -> false
+| Dummy, (Id _ | Tmp _)
+| Id _, (Dummy | Tmp _)
+| Tmp _, (Dummy | Id _)
+ -> false
let rec eq_ml_ast t1 t2 = match t1, t2 with
| MLrel i1, MLrel i2 ->
@@ -394,7 +398,8 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with
| MLdummy k1, MLdummy k2 -> k1 == k2
| MLaxiom, MLaxiom -> true
| MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2
-| _ -> false
+| MLuint i1, MLuint i2 -> Uint63.equal i1 i2
+| _, _ -> false
and eq_ml_pattern p1 p2 = match p1, p2 with
| Pcons (gr1, p1), Pcons (gr2, p2) ->
@@ -426,7 +431,7 @@ let ast_iter_rel f =
| MLapp (a,l) -> iter n a; List.iter (iter n) l
| MLcons (_,_,l) | MLtuple l -> List.iter (iter n) l
| MLmagic a -> iter n a
- | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> ()
+ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> ()
in iter 0
(*s Map over asts. *)
@@ -445,7 +450,7 @@ let ast_map f = function
| MLcons (typ,c,l) -> MLcons (typ,c, List.map f l)
| MLtuple l -> MLtuple (List.map f l)
| MLmagic a -> MLmagic (f a)
- | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a
+ | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ as a -> a
(*s Map over asts, with binding depth as parameter. *)
@@ -463,7 +468,7 @@ let ast_map_lift f n = function
| MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l)
| MLtuple l -> MLtuple (List.map (f n) l)
| MLmagic a -> MLmagic (f n a)
- | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a
+ | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ as a -> a
(*s Iter over asts. *)
@@ -477,7 +482,7 @@ let ast_iter f = function
| MLapp (a,l) -> f a; List.iter f l
| MLcons (_,_,l) | MLtuple l -> List.iter f l
| MLmagic a -> f a
- | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> ()
+ | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> ()
(*S Operations concerning De Bruijn indices. *)
@@ -513,7 +518,7 @@ let nb_occur_match =
| MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
| MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l
| MLmagic a -> nb k a
- | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> 0
+ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> 0
in nb 1
(* Replace unused variables by _ *)
@@ -565,7 +570,7 @@ let dump_unused_vars a =
let b' = ren env b in
if b' == b then a else MLmagic b'
- | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> a
+ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> a
and ren_branch env ((ids,p,b) as tr) =
let occs = List.map (fun _ -> ref false) ids in
@@ -1398,7 +1403,7 @@ let rec ml_size = function
| MLfix(_,_,f) -> ml_size_array f
| MLletin (_,_,t) -> ml_size t
| MLmagic t -> ml_size t
- | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom -> 0
+ | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> 0
and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index b398bc07a0..654695c232 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -108,7 +108,7 @@ let ast_iter_references do_term do_cons do_type a =
Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v
| MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _
- | MLdummy _ | MLaxiom | MLmagic _ -> ()
+ | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ -> ()
in iter a
let ind_iter_references do_term do_cons do_type kn ind =
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 96d8760404..8940aedd6d 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -310,6 +310,10 @@ let rec pp_expr par env args =
apply2
(v 0 (str "match " ++ head ++ str " with" ++ fnl () ++
pp_pat env pv))))
+ | MLuint i ->
+ assert (args=[]);
+ str "(" ++ str (Uint63.compile i) ++ str ")"
+
and pp_record_proj par env typ t pv args =
(* Can a match be printed as a mere record projection ? *)
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 76a0c74068..6aa3a6220e 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -129,6 +129,8 @@ let rec pp_expr env args =
| MLmagic a ->
pp_expr env args a
| MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
+ | MLuint _ ->
+ paren (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
and pp_cons_args env = function
| MLcons (_,r,args) when is_coinductive r ->
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 7b4fd280bd..399a77c596 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -446,14 +446,14 @@ let error_MPfile_as_mod mp b =
let argnames_of_global r =
let env = Global.env () in
- let typ, _ = Global.type_of_global_in_context env r in
+ let typ, _ = Typeops.type_of_global_in_context env r in
let rels,_ =
decompose_prod (Reduction.whd_all env typ) in
- List.rev_map fst rels
+ List.rev_map (fun x -> Context.binder_name (fst x)) rels
let msg_of_implicit = function
| Kimplicit (r,i) ->
- let name = match List.nth (argnames_of_global r) (i-1) with
+ let name = match (List.nth (argnames_of_global r) (i-1)) with
| Anonymous -> ""
| Name id -> "(" ^ Id.to_string id ^ ") "
in
@@ -500,7 +500,7 @@ let info_file f =
let my_bool_option name initval =
let flag = ref initval in
let access = fun () -> !flag in
- let _ = declare_bool_option
+ let () = declare_bool_option
{optdepr = false;
optname = "Extraction "^name;
optkey = ["Extraction"; name];
@@ -572,14 +572,14 @@ let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n
let optims () = !opt_flag_ref
-let _ = declare_bool_option
+let () = declare_bool_option
{optdepr = false;
optname = "Extraction Optimize";
optkey = ["Extraction"; "Optimize"];
optread = (fun () -> not (Int.equal !int_flag_ref 0));
optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))}
-let _ = declare_int_option
+let () = declare_int_option
{ optdepr = false;
optname = "Extraction Flag";
optkey = ["Extraction";"Flag"];
@@ -593,7 +593,7 @@ let _ = declare_int_option
let conservative_types_ref = ref false
let conservative_types () = !conservative_types_ref
-let _ = declare_bool_option
+let () = declare_bool_option
{optdepr = false;
optname = "Extraction Conservative Types";
optkey = ["Extraction"; "Conservative"; "Types"];
@@ -605,7 +605,7 @@ let _ = declare_bool_option
let file_comment_ref = ref ""
let file_comment () = !file_comment_ref
-let _ = declare_string_option
+let () = declare_string_option
{optdepr = false;
optname = "Extraction File Comment";
optkey = ["Extraction"; "File"; "Comment"];
@@ -621,10 +621,9 @@ let lang_ref = Summary.ref Ocaml ~name:"ExtrLang"
let lang () = !lang_ref
let extr_lang : lang -> obj =
- declare_object
- {(default_object "Extraction Lang") with
- cache_function = (fun (_,l) -> lang_ref := l);
- load_function = (fun _ (_,l) -> lang_ref := l)}
+ declare_object @@ superglobal_object_nodischarge "Extraction Lang"
+ ~cache:(fun (_,l) -> lang_ref := l)
+ ~subst:None
let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
@@ -648,15 +647,10 @@ let add_inline_entries b l =
(* Registration of operations for rollback. *)
let inline_extraction : bool * GlobRef.t list -> obj =
- declare_object
- {(default_object "Extraction Inline") with
- cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
- load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
- classify_function = (fun o -> Substitute o);
- discharge_function = (fun (_,x) -> Some x);
- subst_function =
- (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
- }
+ declare_object @@ superglobal_object "Extraction Inline"
+ ~cache:(fun (_,(b,l)) -> add_inline_entries b l)
+ ~subst:(Some (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))))
+ ~discharge:(fun (_,x) -> Some x)
(* Grammar entries. *)
@@ -685,10 +679,9 @@ let print_extraction_inline () =
(* Reset part *)
let reset_inline : unit -> obj =
- declare_object
- {(default_object "Reset Extraction Inline") with
- cache_function = (fun (_,_)-> inline_table := empty_inline_table);
- load_function = (fun _ (_,_)-> inline_table := empty_inline_table)}
+ declare_object @@ superglobal_object_nodischarge "Reset Extraction Inline"
+ ~cache:(fun (_,_)-> inline_table := empty_inline_table)
+ ~subst:None
let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
@@ -731,13 +724,9 @@ let add_implicits r l =
(* Registration of operations for rollback. *)
let implicit_extraction : GlobRef.t * int_or_id list -> obj =
- declare_object
- {(default_object "Extraction Implicit") with
- cache_function = (fun (_,(r,l)) -> add_implicits r l);
- load_function = (fun _ (_,(r,l)) -> add_implicits r l);
- classify_function = (fun o -> Substitute o);
- subst_function = (fun (s,(r,l)) -> (fst (subst_global s r), l))
- }
+ declare_object @@ superglobal_object_nodischarge "Extraction Implicit"
+ ~cache:(fun (_,(r,l)) -> add_implicits r l)
+ ~subst:(Some (fun (s,(r,l)) -> (fst (subst_global s r), l)))
(* Grammar entries. *)
@@ -784,12 +773,9 @@ let add_blacklist_entries l =
(* Registration of operations for rollback. *)
let blacklist_extraction : string list -> obj =
- declare_object
- {(default_object "Extraction Blacklist") with
- cache_function = (fun (_,l) -> add_blacklist_entries l);
- load_function = (fun _ (_,l) -> add_blacklist_entries l);
- subst_function = (fun (_,x) -> x)
- }
+ declare_object @@ superglobal_object_nodischarge "Extraction Blacklist"
+ ~cache:(fun (_,l) -> add_blacklist_entries l)
+ ~subst:None
(* Grammar entries. *)
@@ -805,10 +791,9 @@ let print_extraction_blacklist () =
(* Reset part *)
let reset_blacklist : unit -> obj =
- declare_object
- {(default_object "Reset Extraction Blacklist") with
- cache_function = (fun (_,_)-> blacklist_table := Id.Set.empty);
- load_function = (fun _ (_,_)-> blacklist_table := Id.Set.empty)}
+ declare_object @@ superglobal_object_nodischarge "Reset Extraction Blacklist"
+ ~cache:(fun (_,_)-> blacklist_table := Id.Set.empty)
+ ~subst:None
let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
@@ -852,23 +837,14 @@ let find_custom_match pv =
(* Registration of operations for rollback. *)
let in_customs : GlobRef.t * string list * string -> obj =
- declare_object
- {(default_object "ML extractions") with
- cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
- load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
- classify_function = (fun o -> Substitute o);
- subst_function =
- (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
- }
+ declare_object @@ superglobal_object_nodischarge "ML extractions"
+ ~cache:(fun (_,(r,ids,s)) -> add_custom r ids s)
+ ~subst:(Some (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str)))
let in_custom_matchs : GlobRef.t * string -> obj =
- declare_object
- {(default_object "ML extractions custom matchs") with
- cache_function = (fun (_,(r,s)) -> add_custom_match r s);
- load_function = (fun _ (_,(r,s)) -> add_custom_match r s);
- classify_function = (fun o -> Substitute o);
- subst_function = (fun (subs,(r,s)) -> (fst (subst_global subs r), s))
- }
+ declare_object @@ superglobal_object_nodischarge "ML extractions custom matchs"
+ ~cache:(fun (_,(r,s)) -> add_custom_match r s)
+ ~subst:(Some (fun (subs,(r,s)) -> (fst (subst_global subs r), s)))
(* Grammar entries. *)
@@ -878,7 +854,7 @@ let extract_constant_inline inline r ids s =
match g with
| ConstRef kn ->
let env = Global.env () in
- let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in
+ let typ, _ = Typeops.type_of_global_in_context env (ConstRef kn) in
let typ = Reduction.whd_all env typ in
if Reduction.is_arity env typ
then begin
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 16:14:43 +0000