Formal_ineqs: Remove Pervasives and replace sqrt with float_sqrt

yiyuan-cao · May 10, 2024 · 6b3bc46 · 6b3bc46
1 parent 309b031
commit 6b3bc46
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 7 deletions.
diff --git a/Formal_ineqs/lib/ssreflect/sections.hl b/Formal_ineqs/lib/ssreflect/sections.hl
@@ -44,7 +44,7 @@ let end_section name =
       failwith "end_section: No open sections"
     else
       let last_name, _ = hd sections in
-	if Pervasives.compare last_name name <> 0 then
+	if compare last_name name <> 0 then
 	  failwith ("The last open section is " ^ last_name)
 	else
 	  section_stack := tl sections;;

diff --git a/Formal_ineqs/misc/report.hl b/Formal_ineqs/misc/report.hl
@@ -43,7 +43,7 @@ let report_error =
     fun s ->
       let ec = get_error_count() in
       (inc_error_count(); report_timed (Printf.sprintf "error(%d) --\n%s" ec s); 
-       Pervasives.ignore(get_error_count() < error_max || raise Fatal));;
+       ignore(get_error_count() < error_max || raise Fatal));;
 
 let report_fatal s = 
   ( inc_error_count(); report_timed ("error --\n"^s); raise Fatal);;

diff --git a/Formal_ineqs/trig/unused.hl b/Formal_ineqs/trig/unused.hl
@@ -151,10 +151,10 @@ let n_of_p_log x pp cond =
 
 (*
 
-let sq = Pervasives.sqrt;;
+let sq = float_sqrt;;
 let t = sq (1.0 -. 1.0 /. 3.0) -. 1.0;;
-let t = Pervasives.sqrt 2.0 -. 1.0;;
-let t = Pervasives.sqrt 2.0 /. 2.0 -. 1.0;;
+let t = float_sqrt 2.0 -. 1.0;;
+let t = float_sqrt 2.0 /. 2.0 -. 1.0;;
 t /. (2.0 +. t);;
 
 n_of_p_log 0.11 20 (fun i -> true);;

diff --git a/Formal_ineqs/verifier/m_verifier_main.hl b/Formal_ineqs/verifier/m_verifier_main.hl
@@ -442,7 +442,7 @@ let mk_standard_ineq =
 let expr_to_vector_fun =
   let comp_op = `$` in
     fun expr_tm ->
-      let vars = List.sort Pervasives.compare (frees expr_tm) in
+      let vars = List.sort compare (frees expr_tm) in
       let n = length vars in
       let x_var = mk_var ("x", n_vector_type_array.(if n = 0 then 1 else n)) in
       let x_tm = mk_icomb (comp_op, x_var) in
@@ -455,7 +455,7 @@ let expr_to_vector_fun =
 let exprs_to_vector_fun =
   let comp_op = `$` in
     fun expr_tms ->
-      let vars = List.sort Pervasives.compare (unions (map frees expr_tms)) in
+      let vars = List.sort compare (unions (map frees expr_tms)) in
       let n = length vars in
       let x_var = mk_var ("x", n_vector_type_array.(if n = 0 then 1 else n)) in
       let x_tm = mk_icomb (comp_op, x_var) in