aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/CHANGES4
-rw-r--r--plugins/extraction/ExtrHaskellNatNum.v2
-rw-r--r--plugins/extraction/ExtrOcamlIntConv.v2
-rw-r--r--plugins/extraction/Extraction.v2
-rw-r--r--plugins/extraction/common.ml2
-rw-r--r--plugins/extraction/extract_env.ml35
-rw-r--r--plugins/extraction/extract_env.mli3
-rw-r--r--plugins/extraction/extraction.ml36
-rw-r--r--plugins/extraction/extraction.mli2
-rw-r--r--plugins/extraction/g_extraction.ml410
-rw-r--r--plugins/extraction/haskell.ml5
-rw-r--r--plugins/extraction/miniml.mli2
-rw-r--r--plugins/extraction/mlutil.ml28
-rw-r--r--plugins/extraction/ocaml.ml34
-rw-r--r--plugins/extraction/table.ml13
-rw-r--r--plugins/extraction/table.mli5
16 files changed, 132 insertions, 53 deletions
diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES
index cf97ae3ab8..4bc3dba36e 100644
--- a/plugins/extraction/CHANGES
+++ b/plugins/extraction/CHANGES
@@ -54,7 +54,7 @@ but also a few steps toward a more user-friendly extraction:
* bug fixes:
- many concerning Records.
-- a Stack Overflow with mutual inductive (PR#320)
+- a Stack Overflow with mutual inductive (BZ#320)
- some optimizations have been removed since they were not type-safe:
For example if e has type: type 'x a = A
Then: match e with A -> A -----X----> e
@@ -125,7 +125,7 @@ but also a few steps toward a more user-friendly extraction:
- the dummy constant "__" have changed. see README
- - a few bug-fixes (#191 and others)
+ - a few bug-fixes (BZ#191 and others)
7.2 -> 7.3
diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v
index fabe9a4c67..09b0444614 100644
--- a/plugins/extraction/ExtrHaskellNatNum.v
+++ b/plugins/extraction/ExtrHaskellNatNum.v
@@ -34,4 +34,4 @@ Extract Constant Init.Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
Extract Constant Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
Extract Constant Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
Extract Constant Init.Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
-Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". \ No newline at end of file
+Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v
index fe6eb7780f..ab13d75ada 100644
--- a/plugins/extraction/ExtrOcamlIntConv.v
+++ b/plugins/extraction/ExtrOcamlIntConv.v
@@ -96,4 +96,4 @@ Extraction "/tmp/test.ml"
pos_of_int int_of_pos
z_of_int int_of_z
n_of_int int_of_n.
-*) \ No newline at end of file
+*)
diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v
index 1374a91abf..b3f9d6556d 100644
--- a/plugins/extraction/Extraction.v
+++ b/plugins/extraction/Extraction.v
@@ -6,4 +6,4 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-Declare ML Module "extraction_plugin". \ No newline at end of file
+Declare ML Module "extraction_plugin".
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9772ebd641..9aec190d0a 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -405,7 +405,7 @@ let ref_renaming_fun (k,r) =
let idg = safe_basename_of_global r in
match l with
| [""] -> (* this happens only at toplevel of the monolithic case *)
- let globs = Id.Set.elements (get_global_ids ()) in
+ let globs = get_global_ids () in
let id = next_ident_away (kindcase_id k idg) globs in
Id.to_string id
| _ -> modular_rename k idg
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 89c2a0ae30..bc84df76b7 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Miniml
-open Term
+open Constr
open Declarations
open Names
open ModPath
@@ -138,7 +138,7 @@ let check_arity env cb =
let check_fix env cb i =
match cb.const_body with
| Def lbody ->
- (match kind_of_term (Mod_subst.force_constr lbody) with
+ (match Constr.kind (Mod_subst.force_constr lbody) with
| 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)
@@ -146,8 +146,8 @@ let check_fix env cb i =
let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) =
Array.equal Name.equal na1 na2 &&
- Array.equal eq_constr ca1 ca2 &&
- Array.equal eq_constr ta1 ta2
+ Array.equal Constr.equal ca1 ca2 &&
+ Array.equal Constr.equal ta1 ta2
let factor_fix env l cb msb =
let _,recd as check = check_fix env cb 0 in
@@ -281,7 +281,8 @@ and extract_msignature_spec env mp1 reso = function
MTfunsig (mbid, extract_mbody_spec env mp mtb,
extract_msignature_spec env' mp1 reso me)
-and extract_mbody_spec env mp mb = match mb.mod_type_alg with
+and extract_mbody_spec : 'a. _ -> _ -> 'a generic_module_body -> _ =
+ fun env mp mb -> match mb.mod_type_alg with
| Some ty -> extract_mexpression_spec env mp (mb.mod_type,ty)
| None -> extract_msignature_spec env mp mb.mod_delta mb.mod_type
@@ -341,7 +342,7 @@ let rec extract_structure env mp reso ~all = function
and extract_mexpr env mp = function
| MEwith _ -> assert false (* no 'with' syntax for modules *)
- | me when lang () != Ocaml ->
+ | me when lang () != Ocaml || Table.is_extrcompute () ->
(* In Haskell/Scheme, we expand everything.
For now, we also extract everything, dead code will be removed later
(see [Modutil.optimize_struct]. *)
@@ -569,11 +570,12 @@ let print_structure_to_file (fn,si,mo) dry struc =
let reset () =
Visit.reset (); reset_tables (); reset_renaming_tables Everything
-let init modular library =
+let init ?(compute=false) modular library =
check_inside_section (); check_inside_module ();
set_keywords (descr ()).keywords;
set_modular modular;
set_library library;
+ set_extrcompute compute;
reset ();
if modular && lang () == Scheme then error_scheme ()
@@ -683,8 +685,22 @@ let extraction_library is_rec m =
List.iter print struc;
reset ()
+(** For extraction compute, we flatten all the module structure,
+ getting rid of module types or unapplied functors *)
+
+let flatten_structure struc =
+ let rec flatten_elem (lab,elem) = match elem with
+ |SEdecl d -> [d]
+ |SEmodtype _ -> []
+ |SEmodule m -> match m.ml_mod_expr with
+ |MEfunctor _ -> []
+ |MEident _ | MEapply _ -> assert false (* should be expanded *)
+ |MEstruct (_,elems) -> flatten_elems elems
+ and flatten_elems l = List.flatten (List.map flatten_elem l)
+ in flatten_elems (List.flatten (List.map snd struc))
+
let structure_for_compute c =
- init false false;
+ init false false ~compute:true;
let env = Global.env () in
let ast, mlt = Extraction.extract_constr env c in
let ast = Mlutil.normalize ast in
@@ -693,8 +709,7 @@ let structure_for_compute c =
let () = ast_iter_references add_ref add_ref add_ref ast in
let refs = Refset.elements !refs in
let struc = optimize_struct (refs,[]) (mono_environment refs []) in
- let flatstruc = List.map snd (List.flatten (List.map snd struc)) in
- flatstruc, ast, mlt
+ (flatten_structure struc), ast, mlt
(* For the test-suite :
extraction to a temporary file + run ocamlc on it *)
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 5769ff1176..dd86177381 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -34,5 +34,4 @@ val print_one_decl :
(* Used by Extraction Compute *)
val structure_for_compute :
- Term.constr ->
- Miniml.ml_flat_structure * Miniml.ml_ast * Miniml.ml_type
+ Constr.t -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 7644b49ceb..c169b7b50b 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -10,6 +10,7 @@
open Util
open Names
open Term
+open Constr
open Vars
open Declarations
open Declareops
@@ -81,7 +82,7 @@ let whd_betaiotazeta t =
let rec flag_of_type env t : flag =
let t = whd_all env t in
- match kind_of_term t with
+ match Constr.kind t with
| Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c
| Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
| Sort _ -> (Info,TypeScheme)
@@ -111,14 +112,14 @@ let push_rel_assum (n, t) env =
(*s [type_sign] gernerates a signature aimed at treating a type application. *)
let rec type_sign env c =
- match kind_of_term (whd_all env c) with
+ match Constr.kind (whd_all env c) with
| Prod (n,t,d) ->
(if is_info_scheme env t then Keep else Kill Kprop)
:: (type_sign (push_rel_assum (n,t) env) d)
| _ -> []
let rec type_scheme_nb_args env c =
- match kind_of_term (whd_all env c) with
+ match Constr.kind (whd_all env c) with
| Prod (n,t,d) ->
let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in
if is_info_scheme env t then n+1 else n
@@ -141,10 +142,11 @@ let make_typvar n vl =
if not (String.contains s '\'') && Unicode.is_basic_ascii s then id
else id_of_name Anonymous
in
+ let vl = Id.Set.of_list vl in
next_ident_away id' vl
let rec type_sign_vl env c =
- match kind_of_term (whd_all env c) with
+ match Constr.kind (whd_all env c) with
| Prod (n,t,d) ->
let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
if not (is_info_scheme env t) then Kill Kprop::s, vl
@@ -152,7 +154,7 @@ let rec type_sign_vl env c =
| _ -> [],[]
let rec nb_default_params env c =
- match kind_of_term (whd_all env c) with
+ match Constr.kind (whd_all env c) with
| Prod (n,t,d) ->
let n = nb_default_params (push_rel_assum (n,t) env) d in
if is_default env t then n+1 else n
@@ -206,7 +208,7 @@ let parse_ind_args si args relmax =
| [] -> Int.Map.empty
| Kill _ :: s -> parse (i+1) j s
| Keep :: s ->
- (match kind_of_term args.(i-1) with
+ (match Constr.kind args.(i-1) with
| Rel k -> Int.Map.add (relmax+1-k) j (parse (i+1) (j+1) s)
| _ -> parse (i+1) (j+1) s)
in parse 1 1 si
@@ -223,7 +225,7 @@ let parse_ind_args si args relmax =
let rec extract_type env db j c args =
- match kind_of_term (whd_betaiotazeta c) with
+ match Constr.kind (whd_betaiotazeta c) with
| App (d, args') ->
(* We just accumulate the arguments. *)
extract_type env db j d (Array.to_list args' @ args)
@@ -298,9 +300,9 @@ let rec extract_type env db j c args =
| Proj (p,t) ->
(* Let's try to reduce, if it hasn't already been done. *)
if Projection.unfolded p then Tunknown
- else extract_type env db j (Term.mkProj (Projection.unfold p, t)) args
+ else extract_type env db j (mkProj (Projection.unfold p, t)) args
| Case _ | Fix _ | CoFix _ -> Tunknown
- | _ -> assert false
+ | Var _ | Meta _ | Evar _ | Cast _ | LetIn _ | Construct _ -> assert false
(*s Auxiliary function dealing with type application.
Precondition: [r] is a type scheme represented by the signature [s],
@@ -330,7 +332,7 @@ and extract_type_scheme env db c p =
if Int.equal p 0 then extract_type env db 0 c []
else
let c = whd_betaiotazeta c in
- match kind_of_term c with
+ match Constr.kind c with
| Lambda (n,t,d) ->
extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
| _ ->
@@ -414,8 +416,8 @@ and extract_really_ind env kn mib =
let t = snd (decompose_prod_n npar types.(j)) in
let prods,head = dest_prod epar t in
let nprods = List.length prods in
- let args = match kind_of_term head with
- | App (f,args) -> args (* [kind_of_term f = Ind ip] *)
+ let args = match Constr.kind head with
+ | App (f,args) -> args (* [Constr.kind f = Ind ip] *)
| _ -> [||]
in
let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in
@@ -429,7 +431,7 @@ and extract_really_ind env kn mib =
let ip = (kn, 0) in
let r = IndRef ip in
if is_custom r then raise (I Standard);
- if mib.mind_finite == Decl_kinds.CoFinite then raise (I Coinductive);
+ if mib.mind_finite == CoFinite then raise (I Coinductive);
if not (Int.equal mib.mind_ntypes 1) then raise (I Standard);
let p,u = packets.(0) in
if p.ip_logical then raise (I Standard);
@@ -443,7 +445,7 @@ and extract_really_ind env kn mib =
if Option.is_empty mib.mind_record then raise (I Standard);
(* Now we're sure it's a record. *)
(* First, we find its field names. *)
- let rec names_prod t = match kind_of_term t with
+ let rec names_prod t = match Constr.kind t with
| Prod(n,_,t) -> n::(names_prod t)
| LetIn(_,_,_,t) -> names_prod t
| Cast(t,_,_) -> names_prod t
@@ -502,7 +504,7 @@ and extract_really_ind env kn mib =
*)
and extract_type_cons env db dbmap c i =
- match kind_of_term (whd_all env c) with
+ match Constr.kind (whd_all env 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
@@ -563,7 +565,7 @@ let record_constant_type env kn opt_typ =
(* [mlt] is the ML type we want our extraction of [(c args)] to have. *)
let rec extract_term env mle mlt c args =
- match kind_of_term c with
+ match Constr.kind c with
| App (f,a) ->
extract_term env mle mlt f (Array.to_list a @ args)
| Lambda (n, t, d) ->
@@ -873,7 +875,7 @@ let decomp_lams_eta_n n m env c t =
(* Let's try to identify some situation where extracted code
will allow generalisation of type variables *)
-let rec gentypvar_ok c = match kind_of_term c with
+let rec gentypvar_ok c = match Constr.kind c with
| Lambda _ | Const _ -> true
| App (c,v) ->
(* if all arguments are variables, these variables will
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index e1d43f3405..b15b88ed2c 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -9,7 +9,7 @@
(*s Extraction from Coq terms to Miniml. *)
open Names
-open Term
+open Constr
open Declarations
open Environ
open Miniml
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 23452febdc..24c70bccfb 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -42,14 +42,20 @@ ARGUMENT EXTEND int_or_id
END
let pr_language = function
- | Ocaml -> str "Ocaml"
+ | Ocaml -> str "OCaml"
| Haskell -> str "Haskell"
| Scheme -> str "Scheme"
| JSON -> str "JSON"
+let warn_deprecated_ocaml_spelling =
+ CWarnings.create ~name:"deprecated-ocaml-spelling" ~category:"deprecated"
+ (fun () ->
+ strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\"."))
+
VERNAC ARGUMENT EXTEND language
PRINTED BY pr_language
-| [ "Ocaml" ] -> [ Ocaml ]
+| [ "Ocaml" ] -> [ let _ = warn_deprecated_ocaml_spelling () in Ocaml ]
+| [ "OCaml" ] -> [ Ocaml ]
| [ "Haskell" ] -> [ Haskell ]
| [ "Scheme" ] -> [ Scheme ]
| [ "JSON" ] -> [ JSON ]
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 0f537abece..28abb7f575 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -58,7 +58,6 @@ let preamble mod_name comment used_modules usf =
else
str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++
str "import qualified GHC.Base" ++ fnl () ++
- str "import qualified GHC.Prim" ++ fnl () ++
str "#else" ++ fnl () ++
str "-- HUGS" ++ fnl () ++
str "import qualified IOExts" ++ fnl () ++
@@ -78,7 +77,7 @@ let preamble mod_name comment used_modules usf =
(if not usf.tunknown then mt ()
else
str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++
- str "type Any = GHC.Prim.Any" ++ fnl () ++
+ str "type Any = GHC.Base.Any" ++ fnl () ++
str "#else" ++ fnl () ++
str "-- HUGS" ++ fnl () ++
str "type Any = ()" ++ fnl () ++
@@ -145,7 +144,7 @@ let rec pp_expr par env args =
| MLrel n ->
let id = get_db_name n env in
(* Try to survive to the occurrence of a Dummy rel.
- TODO: we should get rid of this hack (cf. #592) *)
+ TODO: we should get rid of this hack (cf. BZ#592) *)
let id = if Id.equal id dummy_name then Id.of_string "__" else id in
apply (Id.print id)
| MLapp (f,args') ->
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index edebba49df..5e967ef379 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -187,8 +187,6 @@ type ml_structure = (ModPath.t * ml_module_structure) list
type ml_signature = (ModPath.t * ml_module_sig) list
-type ml_flat_structure = ml_structure_elem list
-
type unsafe_needs = {
mldummy : bool;
tdummy : bool;
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index a4c2bcd883..b01b0198d5 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -127,11 +127,15 @@ let rec mgu = function
| Taxiom, Taxiom -> ()
| _ -> raise Impossible
-let needs_magic p = try mgu p; false with Impossible -> true
+let skip_typing () = lang () == Scheme || is_extrcompute ()
-let put_magic_if b a = if b && lang () != Scheme then MLmagic a else a
+let needs_magic p =
+ if skip_typing () then false
+ else try mgu p; false with Impossible -> true
-let put_magic p a = if needs_magic p && lang () != Scheme then MLmagic a else a
+let put_magic_if b a = if b then MLmagic a else a
+
+let put_magic p a = if needs_magic p then MLmagic a else a
let generalizable a =
lang () != Ocaml ||
@@ -769,6 +773,20 @@ let eta_red e =
else e
| _ -> e
+(* Performs an eta-reduction when the core is atomic,
+ or otherwise returns None *)
+
+let atomic_eta_red e =
+ let ids,t = collect_lams e in
+ let n = List.length ids in
+ match t with
+ | MLapp (f,a) when test_eta_args_lift 0 n a ->
+ (match f with
+ | MLrel k when k>n -> Some (MLrel (k-n))
+ | MLglob _ | MLexn _ | MLdummy _ -> Some f
+ | _ -> None)
+ | _ -> None
+
(*s Computes all head linear beta-reductions possible in [(t a)].
Non-linear head beta-redex become let-in. *)
@@ -1053,6 +1071,10 @@ let rec simpl o = function
simpl o (MLcase(typ,e,br'))
| MLmagic(MLdummy _ as e) when lang () == Haskell -> e
| MLmagic(MLexn _ as e) -> e
+ | MLlam _ as e ->
+ (match atomic_eta_red e with
+ | Some e' -> e'
+ | None -> ast_map (simpl o) e)
| a -> ast_map (simpl o) a
(* invariant : list [a] of arguments is non-empty *)
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 9cbc3fd713..5d0f9c167e 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -100,11 +100,41 @@ let pp_global k r = str (str_global k r)
let pp_modname mp = str (Common.pp_module mp)
+(* grammar from OCaml 4.06 manual, "Prefix and infix symbols" *)
+
+let infix_symbols =
+ ['=' ; '<' ; '>' ; '@' ; '^' ; ';' ; '&' ; '+' ; '-' ; '*' ; '/' ; '$' ; '%' ]
+let operator_chars =
+ [ '!' ; '$' ; '%' ; '&' ; '*' ; '+' ; '-' ; '.' ; '/' ; ':' ; '<' ; '=' ; '>' ; '?' ; '@' ; '^' ; '|' ; '~' ]
+
+(* infix ops in OCaml, but disallowed by preceding grammar *)
+
+let builtin_infixes =
+ [ "::" ; "," ]
+
+let substring_all_opchars s start stop =
+ let rec check_char i =
+ if i >= stop then true
+ else
+ List.mem s.[i] operator_chars && check_char (i+1)
+ in
+ check_char start
+
let is_infix r =
is_inline_custom r &&
(let s = find_custom r in
- let l = String.length s in
- l >= 2 && s.[0] == '(' && s.[l-1] == ')')
+ let len = String.length s in
+ len >= 3 &&
+ (* parenthesized *)
+ (s.[0] == '(' && s.[len-1] == ')' &&
+ let inparens = String.trim (String.sub s 1 (len - 2)) in
+ let inparens_len = String.length inparens in
+ (* either, begins with infix symbol, any remainder is all operator chars *)
+ (List.mem inparens.[0] infix_symbols && substring_all_opchars inparens 1 inparens_len) ||
+ (* or, starts with #, at least one more char, all are operator chars *)
+ (inparens.[0] == '#' && inparens_len >= 2 && substring_all_opchars inparens 1 inparens_len) ||
+ (* or, is an OCaml built-in infix *)
+ (List.mem inparens builtin_infixes)))
let get_infix r =
let s = find_custom r in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index ca98f07e8d..5903733a66 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -250,6 +250,11 @@ let modular () = !modular_ref
let set_library b = library_ref := b
let library () = !library_ref
+let extrcompute = ref false
+
+let set_extrcompute b = extrcompute := b
+let is_extrcompute () = !extrcompute
+
(*s Printing. *)
(* The following functions work even on objects not in [Global.env ()].
@@ -481,7 +486,7 @@ let check_loaded_modfile mp = match base_mp mp with
if not (Library.library_is_loaded dp) then begin
match base_mp (Lib.current_mp ()) with
| MPfile dp' when not (DirPath.equal dp dp') ->
- err (str "Please load library " ++ pr_dirpath dp ++ str " first.")
+ err (str "Please load library " ++ DirPath.print dp ++ str " first.")
| _ -> ()
end
| _ -> ()
@@ -750,11 +755,11 @@ let extraction_implicit r l =
let blacklist_table = Summary.ref Id.Set.empty ~name:"ExtrBlacklist"
-let modfile_ids = ref []
+let modfile_ids = ref Id.Set.empty
let modfile_mps = ref MPmap.empty
let reset_modfile () =
- modfile_ids := Id.Set.elements !blacklist_table;
+ modfile_ids := !blacklist_table;
modfile_mps := MPmap.empty
let string_of_modfile mp =
@@ -763,7 +768,7 @@ let string_of_modfile mp =
let id = Id.of_string (raw_string_of_modfile mp) in
let id' = next_ident_away id !modfile_ids in
let s' = Id.to_string id' in
- modfile_ids := id' :: !modfile_ids;
+ modfile_ids := Id.Set.add id' !modfile_ids;
modfile_mps := MPmap.add mp s' !modfile_mps;
s'
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 7e47d0bc81..e52e419fd3 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -165,6 +165,9 @@ val modular : unit -> bool
val set_library : bool -> unit
val library : unit -> bool
+val set_extrcompute : bool -> unit
+val is_extrcompute : unit -> bool
+
(*s Table for custom inlining *)
val to_inline : global_reference -> bool
@@ -177,7 +180,7 @@ val implicits_of_global : global_reference -> Int.Set.t
(*s Table for user-given custom ML extractions. *)
(* UGLY HACK: registration of a function defined in [extraction.ml] *)
-val type_scheme_nb_args_hook : (Environ.env -> Term.constr -> int) Hook.t
+val type_scheme_nb_args_hook : (Environ.env -> Constr.t -> int) Hook.t
val is_custom : global_reference -> bool
val is_inline_custom : global_reference -> bool
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 05:53:54 +0000