summaryrefslogtreecommitdiff
path: root/plugins/extraction/mlutil.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/mlutil.ml')
-rw-r--r--plugins/extraction/mlutil.ml291
1 files changed, 174 insertions, 117 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 1462d3e7..9fdb0205 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1,17 +1,16 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i*)
-open Pp
open Util
open Names
open Libnames
-open Nametab
+open Globnames
open Table
open Miniml
(*i*)
@@ -23,14 +22,14 @@ exception Impossible
(*S Names operations. *)
-let anonymous_name = id_of_string "x"
-let dummy_name = id_of_string "_"
+let anonymous_name = Id.of_string "x"
+let dummy_name = Id.of_string "_"
let anonymous = Id anonymous_name
let id_of_name = function
| Anonymous -> anonymous_name
- | Name id when id = dummy_name -> anonymous_name
+ | Name id when Id.equal id dummy_name -> anonymous_name
| Name id -> id
let id_of_mlid = function
@@ -54,6 +53,22 @@ let new_meta _ =
incr meta_count;
Tmeta {id = !meta_count; contents = None}
+let rec eq_ml_type t1 t2 = match t1, t2 with
+| Tarr (tl1, tr1), Tarr (tl2, tr2) ->
+ eq_ml_type tl1 tl2 && eq_ml_type tr1 tr2
+| Tglob (gr1, t1), Tglob (gr2, t2) ->
+ eq_gr gr1 gr2 && List.equal eq_ml_type t1 t2
+| Tvar i1, Tvar i2 -> Int.equal i1 i2
+| Tvar' i1, Tvar' i2 -> Int.equal i1 i2
+| Tmeta m1, Tmeta m2 -> eq_ml_meta m1 m2
+| Tdummy k1, Tdummy k2 -> k1 == k2
+| Tunknown, Tunknown -> true
+| Taxiom, Taxiom -> true
+| _ -> false
+
+and eq_ml_meta m1 m2 =
+ Int.equal m1.id m2.id && Option.equal eq_ml_type m1.contents m2.contents
+
(* Simultaneous substitution of [[Tvar 1; ... ; Tvar n]] by [l] in a ML type. *)
let type_subst_list l t =
@@ -86,7 +101,7 @@ let instantiation (nb,t) = type_subst_vect (Array.init nb new_meta) t
let rec type_occurs alpha t =
match t with
- | Tmeta {id=beta; contents=None} -> alpha = beta
+ | Tmeta {id=beta; contents=None} -> Int.equal alpha beta
| 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
@@ -95,7 +110,7 @@ let rec type_occurs alpha t =
(*s Most General Unificator *)
let rec mgu = function
- | Tmeta m, Tmeta m' when m.id = m'.id -> ()
+ | Tmeta m, Tmeta m' when Int.equal m.id m'.id -> ()
| Tmeta m, t | t, Tmeta m ->
(match m.contents with
| Some u -> mgu (u, t)
@@ -103,21 +118,24 @@ let rec mgu = function
| None -> m.contents <- Some t)
| Tarr(a, b), Tarr(a', b') ->
mgu (a, a'); mgu (b, b')
- | Tglob (r,l), Tglob (r',l') when r = r' ->
+ | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' ->
List.iter mgu (List.combine l l')
- | (Tdummy _, _ | _, Tdummy _) when lang() = Haskell -> ()
+ | (Tdummy _, _ | _, Tdummy _) when lang() == Haskell -> ()
| Tdummy _, Tdummy _ -> ()
- | t, u when t = u -> () (* for Tvar, Tvar', Tunknown, Taxiom *)
+ | Tvar i, Tvar j when Int.equal i j -> ()
+ | Tvar' i, Tvar' j when Int.equal i j -> ()
+ | Tunknown, Tunknown -> ()
+ | Taxiom, Taxiom -> ()
| _ -> raise Impossible
let needs_magic p = try mgu p; false with Impossible -> true
-let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a
+let put_magic_if b a = if b && lang () != Scheme then MLmagic a else a
-let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a
+let put_magic p a = if needs_magic p && lang () != Scheme then MLmagic a else a
let generalizable a =
- lang () <> Ocaml ||
+ lang () != Ocaml ||
match a with
| MLapp _ -> false
| _ -> true (* TODO, this is just an approximation for the moment *)
@@ -148,7 +166,7 @@ module Mlenv = struct
(* [find_free] finds the free meta in a type. *)
let rec find_free set = function
- | Tmeta m when m.contents = None -> Metaset.add m set
+ | Tmeta m when Option.is_empty m.contents -> Metaset.add m set
| Tmeta {contents = Some t} -> find_free set t
| Tarr (a,b) -> find_free (find_free set a) b
| Tglob (_,l) -> List.fold_left find_free set l
@@ -172,12 +190,12 @@ module Mlenv = struct
let generalization mle t =
let c = ref 0 in
- let map = ref (Intmap.empty : int Intmap.t) in
- let add_new i = incr c; map := Intmap.add i !c !map; !c in
+ let map = ref (Int.Map.empty : int Int.Map.t) in
+ let add_new i = incr c; map := Int.Map.add i !c !map; !c in
let rec meta2var t = match t with
| Tmeta {contents=Some u} -> meta2var u
| Tmeta ({id=i} as m) ->
- (try Tvar (Intmap.find i !map)
+ (try Tvar (Int.Map.find i !map)
with Not_found ->
if Metaset.mem m mle.free then t
else Tvar (add_new i))
@@ -225,21 +243,6 @@ let type_maxvar t =
| _ -> n
in parse 0 t
-(*s What are the type variables occurring in [t]. *)
-
-let intset_union_map_list f l =
- List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l
-
-let intset_union_map_array f a =
- Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a
-
-let rec type_listvar = function
- | Tmeta {contents = Some t} -> type_listvar t
- | Tvar i | Tvar' i -> Intset.singleton i
- | Tarr (a,b) -> Intset.union (type_listvar a) (type_listvar b)
- | Tglob (_,l) -> intset_union_map_list type_listvar l
- | _ -> Intset.empty
-
(*s From [a -> b -> c] to [[a;b],c]. *)
let rec type_decomp = function
@@ -283,13 +286,13 @@ let type_simpl = type_expand (fun _ -> None)
(*s Generating a signature from a ML type. *)
let type_to_sign env t = match type_expand env t with
- | Tdummy d -> Kill d
+ | Tdummy d when not (conservative_types ()) -> Kill d
| _ -> Keep
let type_to_signature env t =
let rec f = function
| Tmeta {contents = Some t} -> f t
- | Tarr (Tdummy d, b) -> Kill d :: f b
+ | Tarr (Tdummy d, b) when not (conservative_types ()) -> Kill d :: f b
| Tarr (_, b) -> Keep :: f b
| _ -> []
in f (type_expand env t)
@@ -318,7 +321,7 @@ let rec sign_kind = function
| NonLogicalSig -> NonLogicalSig
| UnsafeLogicalSig -> UnsafeLogicalSig
| SafeLogicalSig | EmptySig ->
- if k = Kother then UnsafeLogicalSig else SafeLogicalSig
+ if k == Kother then UnsafeLogicalSig else SafeLogicalSig
(* Removing the final [Keep] in a signature *)
@@ -326,17 +329,17 @@ let rec sign_no_final_keeps = function
| [] -> []
| k :: s ->
let s' = k :: sign_no_final_keeps s in
- if s' = [Keep] then [] else s'
+ match s' with [Keep] -> [] | _ -> s'
(*s Removing [Tdummy] from the top level of a ML type. *)
let type_expunge_from_sign env s t =
let rec expunge s t =
- if s = [] then t else match t with
+ if List.is_empty s then t else match t with
| Tmeta {contents = Some t} -> expunge s t
| Tarr (a,b) ->
let t = expunge (List.tl s) b in
- if List.hd s = Keep then Tarr (a, t) else t
+ if List.hd s == Keep then Tarr (a, t) else t
| Tglob (r,l) ->
(match env r with
| Some mlt -> expunge s (type_subst_list l mlt)
@@ -344,7 +347,7 @@ let type_expunge_from_sign env s t =
| _ -> assert false
in
let t = expunge (sign_no_final_keeps s) t in
- if lang () <> Haskell && sign_kind s = UnsafeLogicalSig then
+ if lang () != Haskell && sign_kind s == UnsafeLogicalSig then
Tarr (Tdummy Kother, t)
else t
@@ -353,7 +356,55 @@ let type_expunge env t =
(*S Generic functions over ML ast terms. *)
-let mlapp f a = if a = [] then f else MLapp (f,a)
+let mlapp f a = if List.is_empty a then f else MLapp (f,a)
+
+(** Equality *)
+
+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
+
+let rec eq_ml_ast t1 t2 = match t1, t2 with
+| MLrel i1, MLrel i2 ->
+ Int.equal i1 i2
+| MLapp (f1, t1), MLapp (f2, t2) ->
+ eq_ml_ast f1 f2 && List.equal eq_ml_ast t1 t2
+| MLlam (na1, t1), MLlam (na2, t2) ->
+ eq_ml_ident na1 na2 && eq_ml_ast t1 t2
+| MLletin (na1, c1, t1), MLletin (na2, c2, t2) ->
+ eq_ml_ident na1 na2 && eq_ml_ast c1 c2 && eq_ml_ast t1 t2
+| MLglob gr1, MLglob gr2 -> eq_gr gr1 gr2
+| MLcons (t1, gr1, c1), MLcons (t2, gr2, c2) ->
+ eq_ml_type t1 t2 && eq_gr gr1 gr2 && List.equal eq_ml_ast c1 c2
+| MLtuple t1, MLtuple t2 ->
+ List.equal eq_ml_ast t1 t2
+| MLcase (t1, c1, p1), MLcase (t2, c2, p2) ->
+ eq_ml_type t1 t2 && eq_ml_ast c1 c2 && Array.equal eq_ml_branch p1 p2
+| MLfix (i1, id1, t1), MLfix (i2, id2, t2) ->
+ Int.equal i1 i2 && Array.equal Id.equal id1 id2 && Array.equal eq_ml_ast t1 t2
+| MLexn e1, MLexn e2 -> String.equal e1 e2
+| MLdummy, MLdummy -> true
+| MLaxiom, MLaxiom -> true
+| MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2
+| _ -> false
+
+and eq_ml_pattern p1 p2 = match p1, p2 with
+| Pcons (gr1, p1), Pcons (gr2, p2) ->
+ eq_gr gr1 gr2 && List.equal eq_ml_pattern p1 p2
+| Ptuple p1, Ptuple p2 ->
+ List.equal eq_ml_pattern p1 p2
+| Prel i1, Prel i2 ->
+ Int.equal i1 i2
+| Pwild, Pwild -> true
+| Pusual gr1, Pusual gr2 -> eq_gr gr1 gr2
+| _ -> false
+
+and eq_ml_branch (id1, p1, t1) (id2, p2, t2) =
+ List.equal eq_ml_ident id1 id2 &&
+ eq_ml_pattern p1 p2 &&
+ eq_ml_ast t1 t2
(*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care
of the number of bingings crossed before reaching the [MLrel]. *)
@@ -428,7 +479,7 @@ let ast_iter f = function
let ast_occurs k t =
try
- ast_iter_rel (fun i -> if i = k then raise Found) t; false
+ ast_iter_rel (fun i -> if Int.equal i k then raise Found) t; false
with Found -> true
(*s [occurs_itvl k k' t] returns [true] if there is a [(Rel i)]
@@ -444,7 +495,7 @@ let ast_occurs_itvl k k' t =
let nb_occur_match =
let rec nb k = function
- | MLrel i -> if i = k then 1 else 0
+ | MLrel i -> if Int.equal i k then 1 else 0
| MLcase(_,a,v) ->
(nb k a) +
Array.fold_left
@@ -466,7 +517,7 @@ let ast_lift k t =
let rec liftrec n = function
| MLrel i as a -> if i-n < 1 then a else MLrel (i+k)
| a -> ast_map_lift liftrec n a
- in if k = 0 then t else liftrec 0 t
+ in if Int.equal k 0 then t else liftrec 0 t
let ast_pop t = ast_lift (-1) t
@@ -490,7 +541,7 @@ let ast_subst e =
let rec subst n = function
| MLrel i as a ->
let i' = i-n in
- if i'=1 then ast_lift n e
+ if Int.equal i' 1 then ast_lift n e
else if i'<1 then a
else MLrel (i-1)
| a -> ast_map_lift subst n a
@@ -525,17 +576,18 @@ let has_deep_pattern br =
| Pcons (_,l) | Ptuple l -> not (List.for_all is_basic_pattern l)
| Pusual _ | Prel _ | Pwild -> false
in
- array_exists (function (_,pat,_) -> deep pat) br
+ Array.exists (function (_,pat,_) -> deep pat) br
let is_regular_match br =
- if Array.length br = 0 then false (* empty match becomes MLexn *)
+ if Array.is_empty br then false (* empty match becomes MLexn *)
else
try
let get_r (ids,pat,c) =
match pat with
| Pusual r -> r
| Pcons (r,l) ->
- if not (list_for_all_i (fun i -> (=) (Prel i)) 1 (List.rev l))
+ let is_rel i = function Prel j -> Int.equal i j | _ -> false in
+ if not (List.for_all_i is_rel 1 (List.rev l))
then raise Impossible;
r
| _ -> raise Impossible
@@ -544,7 +596,11 @@ let is_regular_match br =
| ConstructRef (ind,_) -> ind
| _ -> raise Impossible
in
- array_for_all_i (fun i tr -> get_r tr = ConstructRef (ind,i+1)) 0 br
+ let is_ref i tr = match get_r tr with
+ | ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1)
+ | _ -> false
+ in
+ Array.for_all_i is_ref 0 br
with Impossible -> false
(*S Operations concerning lambdas. *)
@@ -562,7 +618,7 @@ let collect_lams =
let collect_n_lams =
let rec collect acc n t =
- if n = 0 then acc,t
+ if Int.equal n 0 then acc,t
else match t with
| MLlam(id,t) -> collect (id::acc) (n-1) t
| _ -> assert false
@@ -571,7 +627,7 @@ let collect_n_lams =
(*s [remove_n_lams] just removes some [MLlam]. *)
let rec remove_n_lams n t =
- if n = 0 then t
+ if Int.equal n 0 then t
else match t with
| MLlam(_,t) -> remove_n_lams (n-1) t
| _ -> assert false
@@ -609,7 +665,7 @@ let rec anonym_or_dummy_lams a = function
(*s The following function creates [MLrel n;...;MLrel 1] *)
let rec eta_args n =
- if n = 0 then [] else (MLrel n)::(eta_args (pred n))
+ if Int.equal n 0 then [] else (MLrel n)::(eta_args (pred n))
(*s Same, but filtered by a signature. *)
@@ -621,25 +677,26 @@ let rec eta_args_sign n = function
(*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *)
let rec test_eta_args_lift k n = function
- | [] -> n=0
- | a :: q -> (a = (MLrel (k+n))) && (test_eta_args_lift k (pred n) q)
+ | [] -> Int.equal n 0
+ | MLrel m :: q -> Int.equal (k+n) m && (test_eta_args_lift k (pred n) q)
+ | _ -> false
(*s Computes an eta-reduction. *)
let eta_red e =
let ids,t = collect_lams e in
let n = List.length ids in
- if n = 0 then e
+ if Int.equal n 0 then e
else match t with
| MLapp (f,a) ->
let m = List.length a in
let ids,body,args =
- if m = n then
+ if Int.equal 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
@@ -715,7 +772,7 @@ let branch_as_fun typ (l,p,c) =
if i'<1 then c
else if i'>nargs then MLrel (i-nargs+1)
else raise Impossible
- | MLcons _ as cons' when cons' = ast_lift n cons -> MLrel (n+1)
+ | MLcons _ as cons' when eq_ml_ast cons' (ast_lift n cons) -> MLrel (n+1)
| a -> ast_map_lift genrec n a
in genrec 0 c
@@ -739,27 +796,33 @@ let branch_as_cst (l,_,c) =
When searching for the best factorisation below, we'll try both.
*)
-(* The following structure allows to record which element occurred
+(* The following structure allows recording which element occurred
at what position, and then finally return the most frequent
element and its positions. *)
let census_add, census_max, census_clean =
- let h = Hashtbl.create 13 in
- let clear () = Hashtbl.clear h in
- let add e i =
- let s = try Hashtbl.find h e with Not_found -> Intset.empty in
- Hashtbl.replace h e (Intset.add i s)
+ let h = ref [] in
+ let clearf () = h := [] in
+ let rec add k v = function
+ | [] -> raise Not_found
+ | (k', s) as p :: l ->
+ if eq_ml_ast k k' then (k', Int.Set.add v s) :: l
+ else p :: add k v l
+ in
+ let addf k i =
+ try h := add k i !h
+ with Not_found -> h := (k, Int.Set.singleton i) :: !h
in
- let max e0 =
- let len = ref 0 and lst = ref Intset.empty and elm = ref e0 in
- Hashtbl.iter
- (fun e s ->
- let n = Intset.cardinal s in
+ let maxf k =
+ let len = ref 0 and lst = ref Int.Set.empty and elm = ref k in
+ List.iter
+ (fun (e, s) ->
+ let n = Int.Set.cardinal s in
if n > !len then begin len := n; lst := s; elm := e end)
- h;
+ !h;
(!elm,!lst)
in
- (add,max,clear)
+ (addf,maxf,clearf)
(* [factor_branches] return the longest possible list of branches
that have the same factorization, either as a function or as a
@@ -771,7 +834,7 @@ let is_opt_pat (_,p,_) = match p with
| _ -> false
let factor_branches o typ br =
- if array_exists is_opt_pat br then None (* already optimized *)
+ if Array.exists is_opt_pat br then None (* already optimized *)
else begin
census_clean ();
for i = 0 to Array.length br - 1 do
@@ -782,8 +845,8 @@ let factor_branches o typ br =
done;
let br_factor, br_set = census_max MLdummy in
census_clean ();
- let n = Intset.cardinal br_set in
- if n = 0 then None
+ let n = Int.Set.cardinal br_set in
+ if Int.equal n 0 then None
else if Array.length br >= 2 && n < 2 then None
else Some (br_factor, br_set)
end
@@ -794,17 +857,17 @@ let rec merge_ids ids ids' = match ids,ids' with
| [],l -> l
| l,[] -> l
| i::ids, i'::ids' ->
- (if i = Dummy then i' else i) :: (merge_ids ids ids')
+ (if i == Dummy then i' else i) :: (merge_ids ids ids')
let is_exn = function MLexn _ -> true | _ -> false
-let rec permut_case_fun br acc =
+let permut_case_fun br acc =
let nb = ref max_int in
Array.iter (fun (_,_,t) ->
let ids, c = collect_lams t in
let n = List.length ids in
if (n < !nb) && (not (is_exn c)) then nb := n) br;
- if !nb = max_int || !nb = 0 then ([],br)
+ if Int.equal !nb max_int || Int.equal !nb 0 then ([],br)
else begin
let br = Array.copy br in
let ids = ref [] in
@@ -837,16 +900,16 @@ let rec iota_red i lift br ((typ,r,a) as cons) =
if i >= Array.length br then raise Impossible;
let (ids,p,c) = br.(i) in
match p with
- | Pusual r' | Pcons (r',_) when r'<>r -> iota_red (i+1) lift br cons
+ | Pusual r' | Pcons (r',_) when not (Globnames.eq_gr r' r) -> iota_red (i+1) lift br cons
| Pusual r' ->
let c = named_lams (List.rev ids) c in
let c = ast_lift lift c
in MLapp (c,a)
- | Prel 1 when List.length ids = 1 ->
+ | Prel 1 when Int.equal (List.length ids) 1 ->
let c = MLlam (List.hd ids, c) in
let c = ast_lift lift c
in MLapp(c,[MLcons(typ,r,a)])
- | Pwild when ids = [] -> ast_lift lift c
+ | Pwild when List.is_empty ids -> ast_lift lift c
| _ -> raise Impossible (* TODO: handle some more cases *)
(* [iota_gen] is an extension of [iota_red] where we allow to
@@ -872,15 +935,11 @@ let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false
Unfolding them leads to more natural code (and more dummy removal) *)
let is_program_branch = function
- | Id id ->
- let s = string_of_id id in
- let br = "program_branch_" in
- let n = String.length br in
- (try
- ignore (int_of_string (String.sub s n (String.length s - n)));
- String.sub s 0 n = br
- with e when Errors.noncritical e -> false)
| Tmp _ | Dummy -> false
+ | Id id ->
+ let s = Id.to_string id in
+ try Scanf.sscanf s "program_branch_%d%!" (fun _ -> true)
+ with Scanf.Scan_failure _ | End_of_file -> false
let expand_linear_let o id e =
o.opt_lin_let || is_tmp id || is_program_branch id || is_imm_apply e
@@ -901,7 +960,7 @@ let rec simpl o = function
if
(is_atomic c) || (is_atomic e) ||
(let n = nb_occur_match e in
- (n = 0 || (n=1 && expand_linear_let o id e)))
+ (Int.equal n 0 || (Int.equal n 1 && expand_linear_let o id e)))
then
simpl o (ast_subst c e)
else
@@ -954,14 +1013,14 @@ and simpl_case o typ br e =
(* Swap the case and the lam if possible *)
let ids,br = if o.opt_case_fun then permut_case_fun br [] else [],br in
let n = List.length ids in
- if n <> 0 then
+ if not (Int.equal n 0) then
simpl o (named_lams ids (MLcase (typ, ast_lift n e, br)))
else
(* Can we merge several branches as the same constant or function ? *)
- if lang() = Scheme || is_custom_match br
+ if lang() == Scheme || is_custom_match br
then MLcase (typ, e, br)
else match factor_branches o typ br with
- | Some (f,ints) when Intset.cardinal ints = Array.length br ->
+ | Some (f,ints) when Int.equal (Int.Set.cardinal ints) (Array.length br) ->
(* If all branches have been factorized, we remove the match *)
simpl o (MLletin (Tmp anonymous_name, e, f))
| Some (f,ints) ->
@@ -970,7 +1029,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.filteri (fun i _ -> not (Int.Set.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)
@@ -996,9 +1055,9 @@ let rec select_via_bl l args = match l,args with
let kill_some_lams bl (ids,c) =
let n = List.length bl in
- let n' = List.fold_left (fun n b -> if b=Keep then (n+1) else n) 0 bl in
- if n = n' then ids,c
- else if n' = 0 then [],ast_lift (-n) c
+ let n' = List.fold_left (fun n b -> if b == Keep then (n+1) else n) 0 bl in
+ if Int.equal n n' then ids,c
+ else if Int.equal n' 0 then [],ast_lift (-n) c
else begin
let v = Array.make n None in
let rec parse_ids i j = function
@@ -1016,15 +1075,15 @@ let kill_some_lams bl (ids,c) =
let kill_dummy_lams c =
let ids,c = collect_lams c in
let bl = List.map sign_of_id ids in
- if not (List.mem Keep bl) then raise Impossible;
+ if not (List.memq Keep bl) then raise Impossible;
let rec fst_kill n = function
| [] -> raise Impossible
| Kill _ :: bl -> n
| 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
@@ -1052,7 +1111,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]
@@ -1061,10 +1120,10 @@ let case_expunge s e =
if all lambdas are logical dummy and the target language is strict. *)
let term_expunge s (ids,c) =
- if s = [] then c
+ if List.is_empty s then c
else
let ids,c = kill_some_lams (List.rev s) (ids,c) in
- if ids = [] && lang () <> Haskell && List.mem (Kill Kother) s then
+ if List.is_empty ids && lang () != Haskell && List.mem (Kill Kother) s then
MLlam (Dummy, ast_lift 1 c)
else named_lams ids c
@@ -1076,7 +1135,7 @@ let kill_dummy_args ids r t =
let m = List.length ids in
let bl = List.rev_map sign_of_id ids in
let rec found n = function
- | MLrel r' when r' = r + n -> true
+ | MLrel r' when Int.equal r' (r + n) -> true
| MLmagic e -> found n e
| _ -> false
in
@@ -1086,7 +1145,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))
@@ -1153,7 +1212,7 @@ let normalize a =
let o = optims () in
let rec norm a =
let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
- if a = a' then a else norm a'
+ if eq_ml_ast a a' then a else norm a'
in norm a
(*S Special treatment of fixpoint for pretty-printing purpose. *)
@@ -1165,7 +1224,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.iteri 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
@@ -1176,7 +1235,7 @@ let optimize_fix a =
else
let ids,a' = collect_lams a in
let n = List.length ids in
- if n = 0 then a
+ if Int.equal n 0 then a
else match a' with
| MLfix(_,[|f|],[|c|]) ->
let new_f = MLapp (MLrel (n+1),eta_args n) in
@@ -1244,7 +1303,7 @@ let rec non_stricts add cand = function
let cand = if add then 1::cand else cand in
pop 1 (non_stricts add cand t)
| MLrel n ->
- List.filter ((<>) n) cand
+ List.filter (fun m -> not (Int.equal m n)) cand
| MLapp (t,l)->
let cand = non_stricts false cand t in
List.fold_left (non_stricts false) cand l
@@ -1268,7 +1327,7 @@ let rec non_stricts add cand = function
let n = List.length i in
let cand = lift n cand in
let cand = pop n (non_stricts add cand t) in
- Sort.merge (<=) cand c) [] v
+ List.merge Int.compare cand c) [] v
(* [merge] may duplicates some indices, but I don't mind. *)
| MLmagic t ->
non_stricts add cand t
@@ -1304,7 +1363,7 @@ let is_not_strict t =
restriction for the moment.
*)
-open Declarations
+open Declareops
let inline_test r t =
if not (auto_inline ()) then false
@@ -1312,7 +1371,7 @@ let inline_test r t =
let c = match r with ConstRef c -> c | _ -> assert false in
let has_body =
try constant_has_body (Global.lookup_constant c)
- with e when Errors.noncritical e -> false
+ with Not_found -> false
in
has_body &&
(let t1 = eta_red t in
@@ -1320,10 +1379,8 @@ let inline_test r t =
not (is_fix t2) && ml_size t < 12 && is_not_strict t)
let con_of_string s =
- let null = empty_dirpath in
- match repr_dirpath (dirpath_of_string s) with
- | id :: d -> make_con (MPfile (make_dirpath d)) null (label_of_id id)
- | [] -> assert false
+ let d, id = Libnames.split_dirpath (dirpath_of_string s) in
+ Constant.make2 (MPfile d) (Label.of_id id)
let manual_inline_set =
List.fold_right (fun x -> Cset_env.add (con_of_string x))
@@ -1355,6 +1412,6 @@ let inline r t =
not (to_keep r) (* The user DOES want to keep it *)
&& not (is_inline_custom r)
&& (to_inline r (* The user DOES want to inline it *)
- || (lang () <> Haskell && not (is_projection r) &&
+ || (lang () != Haskell && not (is_projection r) &&
(is_recursor r || manual_inline r || inline_test r t)))
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 19:37:15 +0000