Commit bb9c876d authored by charguer's avatar charguer

removed new warnings for 8.8.2

parent ff77bcb8
Set Implicit Arguments.
Require Export LibInt FuncDefs FuncPrint.
Require Export LibInt FuncDefs FuncPrint.
Hint Resolve (0%nat) : typeclass_instances.
Hint Resolve (0%Z) : typeclass_instances.
......
......@@ -27,10 +27,10 @@ struct
let bucket h k =
(H.hash k) mod (Array.length h)
let create n =
Array.create n []
let create n =
Array.make n []
let rem h k =
let rem h k =
let b = bucket h k in
h.(b) <- List.filter (fun (k',_) -> not (H.equal k k')) h.(b)
......@@ -42,7 +42,7 @@ struct
let b = bucket h k in
snd (List.find (fun (k',_) -> H.equal k k') h.(b))
let add h k x =
let add h k x =
if not (mem h k) then begin
let b = bucket h k in
h.(b) <- (k,x)::h.(b)
......
......@@ -94,13 +94,13 @@ type t_compact =
mutable c_last_used : int ; }
let create_compact () =
{ c_trans = Array.create 1024 0 ;
c_check = Array.create 1024 (-1) ;
{ c_trans = Array.make 1024 0 ;
c_check = Array.make 1024 (-1) ;
c_last_used = 0 ; }
let reset_compact c =
c.c_trans <- Array.create 1024 0 ;
c.c_check <- Array.create 1024 (-1) ;
c.c_trans <- Array.make 1024 0 ;
c.c_check <- Array.make 1024 (-1) ;
c.c_last_used <- 0
(* One compacted table for transitions, one other for memory actions *)
......@@ -112,9 +112,9 @@ let grow_compact c =
let old_trans = c.c_trans
and old_check = c.c_check in
let n = Array.length old_trans in
c.c_trans <- Array.create (2*n) 0;
c.c_trans <- Array.make (2*n) 0;
Array.blit old_trans 0 c.c_trans 0 c.c_last_used;
c.c_check <- Array.create (2*n) (-1);
c.c_check <- Array.make (2*n) (-1);
Array.blit old_check 0 c.c_check 0 c.c_last_used
let do_pack state_num orig compact =
......@@ -144,8 +144,8 @@ let do_pack state_num orig compact =
(base, default)
let pack_moves state_num move_t =
let move_v = Array.create 257 0
and move_m = Array.create 257 0 in
let move_v = Array.make 257 0
and move_m = Array.make 257 0 in
for i = 0 to 256 do
let act,c = move_t.(i) in
move_v.(i) <- (match act with Backtrack -> -1 | Goto n -> n) ;
......@@ -177,12 +177,12 @@ type lex_tables =
let compact_tables state_v =
let n = Array.length state_v in
let base = Array.create n 0
and backtrk = Array.create n (-1)
and default = Array.create n 0
and base_code = Array.create n 0
and backtrk_code = Array.create n 0
and default_code = Array.create n 0 in
let base = Array.make n 0
and backtrk = Array.make n (-1)
and default = Array.make n 0
and base_code = Array.make n 0
and backtrk_code = Array.make n 0
and default_code = Array.make n 0 in
for i = 0 to n - 1 do
match state_v.(i) with
| Perform (n,c) ->
......
......@@ -84,7 +84,7 @@ let complement s = diff all_chars s
let env_to_array env = match env with
| [] -> assert false
| (_,x)::rem ->
let res = Array.create 257 x in
let res = Array.make 257 x in
List.iter
(fun (c,y) ->
List.iter
......
......@@ -590,7 +590,7 @@ let rec firstpos = function
(* Berry-sethi followpos *)
let followpos size entry_list =
let v = Array.create size TransSet.empty in
let v = Array.make size TransSet.empty in
let rec fill s = function
| Empty|Action _|Tag _ -> ()
| Chars (n,_) -> v.(n) <- s
......@@ -1131,7 +1131,7 @@ let make_tag_entry id start act a r = match a with
| _ -> r
let extract_tags l =
let envs = Array.create (List.length l) TagMap.empty in
let envs = Array.make (List.length l) TagMap.empty in
List.iter
(fun (act,m,_) ->
envs.(act) <-
......@@ -1185,7 +1185,7 @@ let make_dfa lexdef =
done ;
eprintf "%d states\n" !next_state_num ;
*)
let actions = Array.create !next_state_num (Perform (0,[])) in
let actions = Array.make !next_state_num (Perform (0,[])) in
List.iter (fun (act, i) -> actions.(i) <- act) states;
(* Useless state reset, so as to restrict GC roots *)
reset_state () ;
......
......@@ -80,7 +80,7 @@ let output_entry sourcefile ic oc oci e =
output_args e.auto_args
(fun oc x ->
if x > 0 then
fprintf oc "lexbuf.Lexing.lex_mem <- Array.create %d (-1) ; " x)
fprintf oc "lexbuf.Lexing.lex_mem <- Array.make %d (-1) ; " x)
e.auto_mem_size
(output_memory_actions " ") init_moves
e.auto_name
......
......@@ -22,7 +22,7 @@ open Common
let output_auto_defs oc =
fprintf oc "let __ocaml_lex_init_lexbuf lexbuf mem_size =\n\
let pos = lexbuf.Lexing.lex_curr_pos in\n\
lexbuf.Lexing.lex_mem <- Array.create mem_size (-1) ;\n\
lexbuf.Lexing.lex_mem <- Array.make mem_size (-1) ;\n\
lexbuf.Lexing.lex_start_pos <- pos ;\n\
lexbuf.Lexing.lex_last_pos <- pos ;\n\
lexbuf.Lexing.lex_last_action <- -1\n\
......
......@@ -15,12 +15,12 @@ type 'a t = {mutable next : int ; mutable data : 'a array}
let default_size = 32
;;
let create x = {next = 0 ; data = Array.create default_size x}
let create x = {next = 0 ; data = Array.make default_size x}
and reset t = t.next <- 0
;;
let incr_table table new_size =
let t = Array.create new_size table.data.(0) in
let t = Array.make new_size table.data.(0) in
Array.blit table.data 0 t 0 (Array.length table.data) ;
table.data <- t
......
......@@ -91,12 +91,12 @@ let _ =
let outputfile : string =
match !outputfile with
| None ->
Filename.concat dirname ((String.capitalize basename) ^ "_ml.v")
Filename.concat dirname ((String.capitalize_ascii basename) ^ "_ml.v")
| Some f ->
f
in
let debugdir = Filename.concat dirname "_output" in
let debugdirBase = Filename.concat debugdir (String.capitalize basename) in
let debugdirBase = Filename.concat debugdir (String.capitalize_ascii basename) in
(* FAILURE ON WINDOWS *)
let cmd = Printf.sprintf "mkdir -p %s" debugdir in
begin try ignore (Sys.command cmd)
......
......@@ -98,7 +98,7 @@ let process_implementation_file ppf sourcefile =
init_path ();
let prefixname = Filename.chop_extension sourcefile in
let modulename = String.capitalize(Filename.basename prefixname) in
let modulename = String.capitalize_ascii (Filename.basename prefixname) in
Env.set_unit_name modulename;
let inputfile = preprocess sourcefile in
try
......@@ -119,21 +119,21 @@ let process_implementation_file ppf sourcefile =
(*incr Odoc_global.errors ;*)
None, inputfile
(* ADDED *)
| Env.Error err ->
| Env.Error err ->
Env.report_error ppf err;
print_newline();
raise e
| Typecore.Error (loc,err) ->
| Typecore.Error (loc,err) ->
Location.print_error ppf loc;
Typecore.report_error ppf err;
print_newline();
raise e
| Typetexp.Error (loc,err) ->
| Typetexp.Error (loc,err) ->
Location.print_error ppf loc;
Typetexp.report_error ppf err;
print_newline();
raise e
| Typemod.Error (loc,err) ->
| Typemod.Error (loc,err) ->
Location.print_error ppf loc;
Typemod.report_error ppf err;
print_newline();
......@@ -146,7 +146,7 @@ let process_implementation_file ppf sourcefile =
let process_interface_file ppf sourcefile =
init_path ();
let prefixname = Filename.chop_extension sourcefile in
let modulename = String.capitalize(Filename.basename prefixname) in
let modulename = String.capitalize_ascii (Filename.basename prefixname) in
Env.set_unit_name modulename;
let inputfile = preprocess sourcefile in
let ast = parse_file inputfile Parse.interface ast_intf_magic_number in
......@@ -161,7 +161,7 @@ let process_interface_file ppf sourcefile =
let typecheck_implementation_file ppf sourcefile parsetree =
init_path ();
let prefixname = Filename.chop_extension sourcefile in
let modulename = String.capitalize(Filename.basename prefixname) in
let modulename = String.capitalize_ascii (Filename.basename prefixname) in
Env.set_unit_name modulename;
(* let inputfile = preprocess sourcefile in*)
let env = initial_env () in
......@@ -180,21 +180,21 @@ let typecheck_implementation_file ppf sourcefile parsetree =
prerr_endline s;
(*incr Odoc_global.errors ;*)
None
| Env.Error err ->
| Env.Error err ->
Env.report_error ppf err;
print_newline();
raise e
| Typetexp.Error (loc,err) ->
| Typetexp.Error (loc,err) ->
Location.print_error ppf loc;
Typetexp.report_error ppf err;
print_newline();
raise e
| Typecore.Error (loc,err) ->
| Typecore.Error (loc,err) ->
Location.print_error ppf loc;
Typecore.report_error ppf err;
Typecore.report_error ppf err;
print_newline();
raise e
| Typemod.Error (loc,err) ->
| Typemod.Error (loc,err) ->
Location.print_error ppf loc;
Typemod.report_error ppf err;
print_newline();
......@@ -206,7 +206,7 @@ let typecheck_implementation_file ppf sourcefile parsetree =
let typecheck_interface_file ppf sourcefile output_prefix =
init_path ();
let prefixname = Filename.chop_extension sourcefile in
let modulename = String.capitalize(Filename.basename prefixname) in
let modulename = String.capitalize_ascii (Filename.basename prefixname) in
Env.set_unit_name modulename;
let inputfile = preprocess sourcefile in
let ast = parse_file inputfile Parse.interface ast_intf_magic_number in
......@@ -225,21 +225,21 @@ let typecheck_interface_file ppf sourcefile output_prefix =
prerr_endline s;
(*incr Odoc_global.errors ;*)
None
| Env.Error err ->
| Env.Error err ->
Env.report_error ppf err;
print_newline();
raise e
| Typetexp.Error (loc,err) ->
| Typetexp.Error (loc,err) ->
Location.print_error ppf loc;
Typetexp.report_error ppf err;
print_newline();
raise e
| Typecore.Error (loc,err) ->
| Typecore.Error (loc,err) ->
Location.print_error ppf loc;
Typecore.report_error ppf err;
Typecore.report_error ppf err;
print_newline();
raise e
| Typemod.Error (loc,err) ->
| Typemod.Error (loc,err) ->
Location.print_error ppf loc;
Typemod.report_error ppf err;
print_newline();
......
......@@ -325,11 +325,11 @@ type primitive_arity =
let inlined_primitives_table =
[
"Pervasives.ignore", (Primitive_unary, "(@CFML.CFBuiltin.ignore _)");
"Pervasives.+", (Primitive_binary, "Coq.ZArith.BinInt.Zplus");
"Pervasives.-", (Primitive_binary, "Coq.ZArith.BinInt.Zminus");
"Pervasives.*", (Primitive_binary, "Coq.ZArith.BinInt.Zmult");
"Pervasives.~-", (Primitive_unary, "Coq.ZArith.BinInt.Zopp");
"Pervasives.abs", (Primitive_unary, "Coq.ZArith.BinInt.Zabs");
"Pervasives.+", (Primitive_binary, "Coq.ZArith.BinInt.Z.add");
"Pervasives.-", (Primitive_binary, "Coq.ZArith.BinInt.Z.sub");
"Pervasives.*", (Primitive_binary, "Coq.ZArith.BinInt.Z.mul");
"Pervasives.~-", (Primitive_unary, "Coq.ZArith.BinInt.Z.opp");
"Pervasives.abs", (Primitive_unary, "Coq.ZArith.BinInt.Z.abs");
"Pervasives.not", (Primitive_unary, "TLC.LibBool.neg");
"Pervasives.fst", (Primitive_unary, "(@Coq.Init.Datatypes.fst _ _)");
"Pervasives.snd", (Primitive_unary, "(@Coq.Init.Datatypes.snd _ _)");
......
......@@ -220,7 +220,7 @@ let rec pretty_val ppf v = match v.pat_desc with
pretty_val ppf v
| Tpat_alias (v, TPat_type _) -> (* TODO *)
pretty_val ppf v
and pretty_car ppf v = match v.pat_desc with
| Tpat_construct (_,{cstr_tag=tag}, [_ ; _])
when is_cons tag v ->
......@@ -678,8 +678,8 @@ let should_extend ext env = match ext with
(* complement constructor tags *)
let complete_tags nconsts nconstrs tags =
let seen_const = Array.create nconsts false
and seen_constr = Array.create nconstrs false in
let seen_const = Array.make nconsts false
and seen_constr = Array.make nconstrs false in
List.iter
(function
| Cstr_constant i -> seen_const.(i) <- true
......@@ -886,7 +886,7 @@ let build_other ext env = match env with
let snd3 (_,x,_) = x
let thd3 (_,_,x) = x
let rec has_instance p = match p.pat_desc with
| Tpat_variant (l,_,r) when is_absent l r -> false
| Tpat_any | Tpat_var _ | Tpat_constant _ | Tpat_variant (_,None,_) -> true
......@@ -1604,7 +1604,7 @@ let rec collect_paths_from_pat r p = match p.pat_desc with
| Tpat_variant (_, Some p, _) | Tpat_alias (p,_) -> collect_paths_from_pat r p
| Tpat_or (p1,p2,_) ->
collect_paths_from_pat (collect_paths_from_pat r p1) p2
| Tpat_lazy p
| Tpat_lazy p
->
collect_paths_from_pat r p
......
......@@ -126,8 +126,8 @@ let letter = function
| _ -> assert false
;;
let active = Array.create (last_warning_number + 1) true;;
let error = Array.create (last_warning_number + 1) false;;
let active = Array.make (last_warning_number + 1) true;;
let error = Array.make (last_warning_number + 1) false;;
let is_active x = active.(number x);;
let is_error x = error.(number x);;
......
......@@ -198,9 +198,9 @@ Qed.
(** Pred / Succ *)
Definition pred (n:int) := (Coq.ZArith.BinInt.Zminus n 1).
Definition pred (n:int) := (Coq.ZArith.BinInt.Z.sub n 1).
Definition succ (n:int) := (Coq.ZArith.BinInt.Zplus n 1).
Definition succ (n:int) := (Coq.ZArith.BinInt.Z.add n 1).
(** Ignore *)
......@@ -212,10 +212,10 @@ Definition ignore A (x:A) := tt.
(* Preventing simplifications *)
Global Opaque
Coq.ZArith.BinInt.Zplus
Coq.ZArith.BinInt.Zminus
Coq.ZArith.BinInt.Zmult
Coq.ZArith.BinInt.Zopp.
Coq.ZArith.BinInt.Z.add
Coq.ZArith.BinInt.Z.sub
Coq.ZArith.BinInt.Z.mul
Coq.ZArith.BinInt.Z.opp.
Global Transparent Coq.ZArith.BinInt.Z.sub.
......
......@@ -10,6 +10,7 @@ include $(CFML)/Makefile.common
PWD := $(shell pwd)
V := $(wildcard $(PWD)/*.v)
COQFLAGS := -w -notation-overridden
ifdef INCLUDE_TLC_AS_DEPENDENCIES
# For Arthur: encompass TLC in the scope of the dependency graph.
......
......@@ -75,7 +75,7 @@ Parameter infix_neq_spec : curried 2%nat infix_eq__ /\
Hint Extern 1 (RegisterSpec infix_lt_gt__) => Provide infix_neq_spec.
Lemma min_spec : forall (n m:int),
app min [n m] \[] \[= Zmin n m ].
app min [n m] \[] \[= Z.min n m ].
Proof using.
xcf. xgo*.
{ rewrite~ Z.min_l. }
......@@ -83,7 +83,7 @@ Proof using.
Qed.
Lemma max_spec : forall (n m:int),
app max [n m] \[] \[= Zmax n m ].
app max [n m] \[] \[= Z.max n m ].
Proof using.
xcf. xgo*.
{ rewrite~ Z.max_l. }
......@@ -112,19 +112,19 @@ Hint Extern 1 (RegisterSpec infix_amp_amp__) => Provide infix_amp_amp_spec.
Parameter infix_tilde_minus_spec : curried 1%nat infix_tilde_minus__ /\
forall (n:int),
app infix_tilde_minus__ [n] \[] \[= Zopp n ].
app infix_tilde_minus__ [n] \[] \[= Z.opp n ].
Parameter infix_plus_spec : curried 2%nat infix_plus__ /\
forall (n m:int),
app infix_plus__ [n m] \[] \[= Zplus n m ].
app infix_plus__ [n m] \[] \[= Z.add n m ].
Parameter infix_minus_spec : curried 2%nat infix_minus__ /\
forall (n m:int),
app infix_minus__ [n m] \[] \[= Zminus n m ].
app infix_minus__ [n m] \[] \[= Z.sub n m ].
Parameter infix_star_spec : curried 2%nat infix_star__ /\
forall (n m:int),
app infix_star__ [n m] \[] \[= Zmult n m ].
app infix_star__ [n m] \[] \[= Z.mul n m ].
Parameter infix_slash_spec : curried 2%nat infix_slash__ /\
forall (n m:int),
......@@ -177,7 +177,7 @@ Proof using.
Qed.
Lemma abs_spec : forall (n:int),
app Pervasives_ml.abs [n] \[] \[= Zabs n ].
app Pervasives_ml.abs [n] \[] \[= Z.abs n ].
Proof using.
xcf. xgo.
{ rewrite~ Z.abs_eq. }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment