diff options
Diffstat (limited to 'plugins/extraction')
-rw-r--r-- | plugins/extraction/extract_env.ml | 6 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 14 | ||||
-rw-r--r-- | plugins/extraction/haskell.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/mlutil.ml | 6 | ||||
-rw-r--r-- | plugins/extraction/modutil.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/ocaml.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/scheme.ml | 2 |
7 files changed, 17 insertions, 17 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index b5cdec3ec..aaf6f2bd0 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -141,8 +141,8 @@ let check_fix env cb i = let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) = na1 = na2 && - array_equal eq_constr ca1 ca2 && - array_equal eq_constr ta1 ta2 + Array.equal eq_constr ca1 ca2 && + Array.equal eq_constr ta1 ta2 let factor_fix env l cb msb = let _,recd as check = check_fix env cb 0 in @@ -287,7 +287,7 @@ let rec extract_sfb env mp all = function let vl,recd,msb = factor_fix env l cb msb in let vc = Array.map (make_con mp empty_dirpath) vl in let ms = extract_sfb env mp all msb in - let b = array_exists Visit.needed_con vc in + let b = Array.exists Visit.needed_con vc in if all || b then let d = extract_fixpoint env vc recd in if (not b) && (logical_decl d) then ms diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index e1bbcf9c7..ef0de36f5 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -202,7 +202,7 @@ let oib_equal o1 o2 = o1.mind_consnames = o2.mind_consnames let mib_equal m1 m2 = - array_equal oib_equal m1.mind_packets m1.mind_packets && + Array.equal oib_equal m1.mind_packets m1.mind_packets && m1.mind_record = m2.mind_record && m1.mind_finite = m2.mind_finite && m1.mind_ntypes = m2.mind_ntypes && @@ -833,7 +833,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt = let metas = Array.map new_meta fi in metas.(i) <- mlt; let mle = Array.fold_left Mlenv.push_type mle metas in - let ei = array_map2 (extract_maybe_term env mle) metas ci in + let ei = Array.map2 (extract_maybe_term env mle) metas ci in MLfix (i, Array.map id_of_name fi, ei) (*S ML declarations. *) @@ -859,7 +859,7 @@ let rec gentypvar_ok c = match kind_of_term c with | App (c,v) -> (* if all arguments are variables, these variables will disappear after extraction (see [empty_s] below) *) - array_for_all isRel v && gentypvar_ok c + Array.for_all isRel v && gentypvar_ok c | Cast (c,_,_) -> gentypvar_ok c | _ -> false @@ -1053,9 +1053,9 @@ let logical_decl = function | Dterm (_,MLdummy,Tdummy _) -> true | Dtype (_,[],Tdummy _) -> true | Dfix (_,av,tv) -> - (array_for_all ((=) MLdummy) av) && - (array_for_all isDummy tv) - | Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets + (Array.for_all ((=) MLdummy) av) && + (Array.for_all isDummy tv) + | Dind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets | _ -> false (*s Is a [ml_spec] logical ? *) @@ -1063,5 +1063,5 @@ let logical_decl = function let logical_spec = function | Stype (_, [], Some (Tdummy _)) -> true | Sval (_,Tdummy _) -> true - | Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets + | Sind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets | _ -> false diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 2bc2306f1..4fd9f17ee 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -224,7 +224,7 @@ and pp_fix par env i (ids,bl) args = (v 1 (str "let {" ++ fnl () ++ prvect_with_sep (fun () -> str ";" ++ fnl ()) (fun (fi,ti) -> pp_function env (pr_id fi) ti) - (array_map2 (fun a b -> a,b) ids bl) ++ + (Array.map2 (fun a b -> a,b) ids bl) ++ str "}") ++ fnl () ++ str "in " ++ pp_apply (pr_id ids.(i)) false args)) diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 3716695b8..01b98b131 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -524,7 +524,7 @@ 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 *) @@ -543,7 +543,7 @@ 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 + Array.for_all_i (fun i tr -> get_r tr = ConstructRef (ind,i+1)) 0 br with Impossible -> false (*S Operations concerning lambdas. *) @@ -770,7 +770,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 diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 8659de03e..9247baba2 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -270,7 +270,7 @@ let rec optim_se top to_appear s = function else all := false done; if !all && top && not (library ()) - && (array_for_all (fun r -> not (List.mem r to_appear)) rv) + && (Array.for_all (fun r -> not (List.mem r to_appear)) rv) then optim_se top to_appear s lse else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse) | (l,SEmodule m) :: lse -> diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 951049b7b..78126bc16 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -374,7 +374,7 @@ and pp_fix par env i (ids,bl) args = prvect_with_sep (fun () -> fnl () ++ str "and ") (fun (fi,ti) -> pr_id fi ++ pp_function env ti) - (array_map2 (fun id b -> (id,b)) ids bl) ++ + (Array.map2 (fun id b -> (id,b)) ids bl) ++ fnl () ++ hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args))) diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index ec338b1db..a0a59e73c 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -163,7 +163,7 @@ and pp_fix env j (ids,bl) args = (prvect_with_sep fnl (fun (fi,ti) -> paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti))) - (array_map2 (fun id b -> (id,b)) ids bl)) ++ + (Array.map2 (fun id b -> (id,b)) ids bl)) ++ fnl () ++ hov 2 (pp_apply (pr_id (ids.(j))) true args)))) |