aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/common.ml4
-rw-r--r--plugins/extraction/extract_env.ml6
-rw-r--r--plugins/extraction/extraction.ml26
-rw-r--r--plugins/extraction/mlutil.ml18
-rw-r--r--plugins/extraction/modutil.ml2
-rw-r--r--plugins/extraction/ocaml.ml6
-rw-r--r--plugins/extraction/table.ml4
7 files changed, 33 insertions, 33 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index b6b7e58338..8cceb2a111 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -349,7 +349,7 @@ let rec mp_renaming_fun mp = match mp with
| MPfile _ ->
assert (modular ()); (* see [at_toplevel] above *)
assert (get_phase () = Pre);
- let current_mpfile = (list_last (get_visible ())).mp in
+ let current_mpfile = (List.last (get_visible ())).mp in
if mp <> current_mpfile then mpfiles_add mp;
[string_of_modfile mp]
@@ -496,7 +496,7 @@ let fstlev_ks k = function
let pp_ocaml_local k prefix mp rls olab =
(* what is the largest prefix of [mp] that belongs to [visible]? *)
assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *)
- let rls' = list_skipn (mp_length prefix) rls in
+ let rls' = List.skipn (mp_length prefix) rls in
let k's = fstlev_ks k rls' in
(* Reference r / module path mp is of the form [<prefix>.s.<...>]. *)
if not (visible_clash prefix k's) then dottify rls'
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 588fe0cf23..b5cdec3ece 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -150,9 +150,9 @@ let factor_fix env l cb msb =
if n = 1 then [|l|], recd, msb
else begin
if List.length msb < n-1 then raise Impossible;
- let msb', msb'' = list_chop (n-1) msb in
+ let msb', msb'' = List.chop (n-1) msb in
let labels = Array.make n l in
- list_iter_i
+ List.iter_i
(fun j ->
function
| (l,SFBconst cb') ->
@@ -207,7 +207,7 @@ let env_for_mtb_with_def env mp seb idl =
in
let l = label_of_id (List.hd idl) in
let spot = function (l',SFBconst _) -> l = l' | _ -> false in
- let before = fst (list_split_when spot sig_b) in
+ let before = fst (List.split_when spot sig_b) in
Modops.add_signature mp before empty_delta_resolver env
(* From a [structure_body] (i.e. a list of [structure_field_body])
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 0556f6d77f..e1bbcf9c75 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -193,7 +193,7 @@ let parse_ind_args si args relmax =
let oib_equal o1 o2 =
id_ord o1.mind_typename o2.mind_typename = 0 &&
- list_equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
+ List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
begin match o1.mind_arity, o2.mind_arity with
| Monomorphic {mind_user_arity=c1; mind_sort=s1},
Monomorphic {mind_user_arity=c2; mind_sort=s2} ->
@@ -206,10 +206,10 @@ let mib_equal m1 m2 =
m1.mind_record = m2.mind_record &&
m1.mind_finite = m2.mind_finite &&
m1.mind_ntypes = m2.mind_ntypes &&
- list_equal eq_named_declaration m1.mind_hyps m2.mind_hyps &&
+ List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps &&
m1.mind_nparams = m2.mind_nparams &&
m1.mind_nparams_rec = m2.mind_nparams_rec &&
- list_equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
+ List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
m1.mind_constraints = m2.mind_constraints
(*S Extraction of a type. *)
@@ -439,7 +439,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
| _ -> []
in
let field_names =
- list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
+ List.skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
assert (List.length field_names = List.length typ);
let projs = ref Cset.empty in
let mp,d,_ = repr_mind kn in
@@ -674,7 +674,7 @@ and extract_cst_app env mle mlt kn args =
let mla =
if not magic1 then
try
- let l,l' = list_chop (projection_arity (ConstRef kn)) mla in
+ let l,l' = List.chop (projection_arity (ConstRef kn)) mla in
if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
else mla
with _ -> mla
@@ -697,7 +697,7 @@ and extract_cst_app env mle mlt kn args =
(* Partially applied function with some logical arg missing.
We complete via eta and expunge logical args. *)
let ls' = ls-la in
- let s' = list_skipn la s in
+ let s' = List.skipn la s in
let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
let e = anonym_or_dummy_lams (mlapp head mla) s' in
put_magic_if magic2 (remove_n_lams (List.length optdummy) e)
@@ -729,7 +729,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
let la = List.length args in
assert (la <= ls + params_nb);
let la' = max 0 (la - params_nb) in
- let args' = list_lastn la' args in
+ let args' = List.lastn la' args in
(* Now, we build the expected type of the constructor *)
let metas = List.map new_meta args' in
(* If stored and expected types differ, then magic! *)
@@ -758,7 +758,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
then put_magic_if (magic2 && not magic1) (head mla)
else (* [ params_nb <= la <= ls + params_nb ] *)
let ls' = params_nb + ls - la in
- let s' = list_lastn ls' s in
+ let s' = List.lastn ls' s in
let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
put_magic_if magic2 (anonym_or_dummy_lams (head mla) s')
@@ -847,7 +847,7 @@ let decomp_lams_eta_n n m env c t =
let rels',c = decompose_lam c in
let d = n - m in
(* we'd better keep rels' as long as possible. *)
- let rels = (list_firstn d rels) @ rels' in
+ let rels = (List.firstn d rels) @ rels' in
let eta_args = List.rev_map mkRel (interval 1 d) in
rels, applist (lift d c,eta_args)
@@ -886,7 +886,7 @@ let extract_std_constant env kn body typ =
and m = nb_lam body in
if n <= m then decompose_lam_n n body
else
- let s,s' = list_chop m s in
+ let s,s' = List.chop m s in
if List.for_all ((=) Keep) s' &&
(lang () = Haskell || sign_kind s <> UnsafeLogicalSig)
then decompose_lam_n m body
@@ -895,7 +895,7 @@ let extract_std_constant env kn body typ =
(* Should we do one eta-expansion to avoid non-generalizable '_a ? *)
let rels, c =
let n = List.length rels in
- let s,s' = list_chop n s in
+ let s,s' = List.chop n s in
let k = sign_kind s in
let empty_s = (k = EmptySig || k = SafeLogicalSig) in
if lang () = Ocaml && empty_s && not (gentypvar_ok c)
@@ -904,8 +904,8 @@ let extract_std_constant env kn body typ =
else rels,c
in
let n = List.length rels in
- let s = list_firstn n s in
- let l,l' = list_chop n l in
+ let s = List.firstn n s in
+ let l,l' = List.chop n l in
let t' = type_recomp (l',t') in
(* The initial ML environment. *)
let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 3b89386d40..3716695b86 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -534,7 +534,7 @@ let is_regular_match br =
match pat with
| Pusual r -> r
| Pcons (r,l) ->
- if not (list_for_all_i (fun i -> (=) (Prel i)) 1 (List.rev l))
+ if not (List.for_all_i (fun i -> (=) (Prel i)) 1 (List.rev l))
then raise Impossible;
r
| _ -> raise Impossible
@@ -636,9 +636,9 @@ let eta_red e =
if m = n then
[], f, a
else if m < n then
- list_skipn m ids, f, a
+ List.skipn m ids, f, a
else (* m > n *)
- let a1,a2 = list_chop (m-n) a in
+ let a1,a2 = List.chop (m-n) a in
[], MLapp (f,a1), a2
in
let p = List.length args in
@@ -969,7 +969,7 @@ and simpl_case o typ br e =
else ([], Pwild, ast_pop f)
in
let brl = Array.to_list br in
- let brl_opt = list_filter_i (fun i _ -> not (Intset.mem i ints)) brl in
+ let brl_opt = List.filter_i (fun i _ -> not (Intset.mem i ints)) brl in
let brl_opt = brl_opt @ [last_br] in
MLcase (typ, e, Array.of_list brl_opt)
| None -> MLcase (typ, e, br)
@@ -1022,8 +1022,8 @@ let kill_dummy_lams c =
| Keep :: bl -> fst_kill (n+1) bl
in
let skip = max 0 ((fst_kill 0 bl) - 1) in
- let ids_skip, ids = list_chop skip ids in
- let _, bl = list_chop skip bl in
+ let ids_skip, ids = List.chop skip ids in
+ let _, bl = List.chop skip bl in
let c = named_lams ids_skip c in
let ids',c = kill_some_lams bl (ids,c) in
ids, named_lams ids' c
@@ -1051,7 +1051,7 @@ let case_expunge s e =
let m = List.length s in
let n = nb_lams e in
let p = if m <= n then collect_n_lams m e
- else eta_expansion_sign (list_skipn n s) (collect_lams e) in
+ else eta_expansion_sign (List.skipn n s) (collect_lams e) in
kill_some_lams (List.rev s) p
(*s [term_expunge] takes a function [fun idn ... id1 -> c]
@@ -1085,7 +1085,7 @@ let kill_dummy_args ids r t =
let a = List.map (killrec n) a in
let a = List.map (ast_lift k) a in
let a = select_via_bl bl (a @ (eta_args k)) in
- named_lams (list_firstn k ids) (MLapp (ast_lift k e, a))
+ named_lams (List.firstn k ids) (MLapp (ast_lift k e, a))
| e when found n e ->
let a = select_via_bl bl (eta_args m) in
named_lams ids (MLapp (ast_lift m e, a))
@@ -1164,7 +1164,7 @@ let general_optimize_fix f ids n args m c =
| MLrel j when v.(j-1)>=0 ->
if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1)
| _ -> raise Impossible
- in list_iter_i aux args;
+ in List.iter_i aux args;
let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
let new_f = anonym_tmp_lams (MLapp (MLrel (n+m+1),args_f)) m in
let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 1211bbf173..8659de03eb 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -30,7 +30,7 @@ let se_iter do_decl do_spec =
| MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
| MTwith (mt,ML_With_type(idl,l,t))->
let mp_mt = msid_of_mt mt in
- let l',idl' = list_sep_last idl in
+ let l',idl' = List.sep_last idl in
let mp_w =
List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
in
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 34ae1f9ad8..951049b7b2 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -114,7 +114,7 @@ let pp_one_field r i = function
let pp_field r fields i = pp_one_field r i (List.nth fields i)
-let pp_fields r fields = list_map_i (pp_one_field r) 0 fields
+let pp_fields r fields = List.map_i (pp_one_field r) 0 fields
(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
are needed or not. *)
@@ -189,7 +189,7 @@ let rec pp_expr par env args =
hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2))
| MLglob r ->
(try
- let args = list_skipn (projection_arity r) args in
+ let args = List.skipn (projection_arity r) args in
let record = List.hd args in
pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
with _ -> apply (pp_global Term r))
@@ -642,7 +642,7 @@ and pp_module_type params = function
| MTwith(mt,ML_With_type(idl,vl,typ)) ->
let ids = pp_parameters (rename_tvars keywords vl) in
let mp_mt = msid_of_mt mt in
- let l,idl' = list_sep_last idl in
+ let l,idl' = List.sep_last idl in
let mp_w =
List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 2dd07b2f2b..6151abf6eb 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -671,7 +671,7 @@ let add_implicits r l =
else err (int i ++ str " is not a valid argument number for " ++
safe_pr_global r)
| ArgId id ->
- (try list_index (Name id) names
+ (try List.index (Name id) names
with Not_found ->
err (str "No argument " ++ pr_id id ++ str " for " ++
safe_pr_global r))
@@ -877,7 +877,7 @@ let extract_inductive r s l optstr =
Lib.add_anonymous_leaf (in_customs (g,[],s));
Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s)))
optstr;
- list_iter_i
+ List.iter_i
(fun j s ->
let g = ConstructRef (ip,succ j) in
Lib.add_anonymous_leaf (inline_extraction (true,[g]));
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 19:01:55 +0000