summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/dp/dp.ml18
-rw-r--r--contrib/extraction/common.ml10
-rw-r--r--contrib/extraction/extract_env.ml17
-rw-r--r--contrib/extraction/mlutil.ml4
-rw-r--r--contrib/funind/recdef.ml26
-rw-r--r--contrib/xml/xml.ml42
-rw-r--r--contrib/xml/xmlcommand.ml10
7 files changed, 49 insertions, 38 deletions
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 79ffaf3f..d8803847 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -701,7 +701,7 @@ let file_contents f =
let timeout_sys_command cmd =
if !debug then Format.eprintf "command line: %s@." cmd;
let out = Filename.temp_file "out" "" in
- let cmd = sprintf "cpulimit %d %s > %s 2>&1" !timeout cmd out in
+ let cmd = sprintf "why-cpulimit %d %s > %s 2>&1" !timeout cmd out in
let ret = Sys.command cmd in
if !debug then
Format.eprintf "Output file %s:@.%s@." out (file_contents out);
@@ -731,12 +731,12 @@ let why_files f = String.concat " " (!prelude_files @ [f])
let call_simplify fwhy =
let cmd =
- sprintf "why --no-arrays --simplify --encoding sstrat %s" (why_files fwhy)
+ sprintf "why --simplify %s" (why_files fwhy)
in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in
let cmd =
- sprintf "timeout %d Simplify %s > out 2>&1 && grep -q -w Valid out"
+ sprintf "why-cpulimit %d Simplify %s > out 2>&1 && grep -q -w Valid out"
!timeout fsx
in
let out = Sys.command cmd in
@@ -747,7 +747,7 @@ let call_simplify fwhy =
r
let call_ergo fwhy =
- let cmd = sprintf "why --no-arrays --why %s" (why_files fwhy) in
+ let cmd = sprintf "why --alt-ergo %s" (why_files fwhy) in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fwhy = Filename.chop_suffix fwhy ".why" ^ "_why.why" in
let ftrace = Filename.temp_file "ergo_trace" "" in
@@ -797,12 +797,12 @@ let call_zenon fwhy =
let call_yices fwhy =
let cmd =
- sprintf "why --no-arrays -smtlib --encoding sstrat %s" (why_files fwhy)
+ sprintf "why -smtlib --encoding sstrat %s" (why_files fwhy)
in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fsmt = Filename.chop_suffix fwhy ".why" ^ "_why.smt" in
let cmd =
- sprintf "timeout %d yices -pc 0 -smt < %s > out 2>&1 && grep -q -w unsat out"
+ sprintf "why-cpulimit %d yices -pc 0 -smt %s > out 2>&1 && grep -q -w unsat out"
!timeout fsmt
in
let out = Sys.command cmd in
@@ -814,7 +814,7 @@ let call_yices fwhy =
let call_cvcl fwhy =
let cmd =
- sprintf "why --no-arrays --cvcl --encoding sstrat %s" (why_files fwhy)
+ sprintf "why --cvcl --encoding sstrat %s" (why_files fwhy)
in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in
@@ -831,7 +831,7 @@ let call_cvcl fwhy =
let call_harvey fwhy =
let cmd =
- sprintf "why --no-arrays --harvey --encoding strat %s" (why_files fwhy)
+ sprintf "why --harvey --encoding strat %s" (why_files fwhy)
in
if Sys.command cmd <> 0 then error ("call to " ^ cmd ^ " failed");
let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in
@@ -856,7 +856,7 @@ let call_harvey fwhy =
r
let call_gwhy fwhy =
- let cmd = sprintf "gwhy --no-arrays %s" (why_files fwhy) in
+ let cmd = sprintf "gwhy %s" (why_files fwhy) in
if Sys.command cmd <> 0 then ignore (Sys.command (sprintf "emacs %s" fwhy));
NoAnswer
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 02173c1f..73f44e68 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: common.ml 11559 2008-11-07 22:03:34Z letouzey $ i*)
+(*i $Id: common.ml 13200 2010-06-25 22:36:25Z letouzey $ i*)
open Pp
open Util
@@ -21,6 +21,8 @@ open Mlutil
open Modutil
open Mod_subst
+let string_of_id id = ascii_of_ident (Names.string_of_id id)
+
(*s Some pretty-print utility functions. *)
let pp_par par st = if par then str "(" ++ st ++ str ")" else st
@@ -73,7 +75,11 @@ let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
-let uppercase_id id = id_of_string (String.capitalize (string_of_id id))
+let uppercase_id id =
+ let s = string_of_id id in
+ assert (s<>"");
+ if s.[0] = '_' then id_of_string ("Coq_"^s)
+ else id_of_string (String.capitalize s)
type kind = Term | Type | Cons | Mod
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 49a86200..057a7b29 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extract_env.ml 11846 2009-01-22 18:55:10Z letouzey $ i*)
+(*i $Id: extract_env.ml 13201 2010-06-25 22:36:27Z letouzey $ i*)
open Term
open Declarations
@@ -489,15 +489,12 @@ let simple_extraction r = match locate_ref [r] with
| ([], [mp]) as p -> full_extr None p
| [r],[] ->
init false;
- if is_custom r then
- msgnl (str "User defined extraction:" ++ spc () ++
- str (find_custom r) ++ fnl ())
- else
- let struc = optimize_struct [r] (mono_environment [r] []) in
- let d = get_decl_in_structure r struc in
- warning_axioms ();
- print_one_decl struc (modpath_of_r r) d;
- reset ()
+ let struc = optimize_struct [r] (mono_environment [r] []) in
+ let d = get_decl_in_structure r struc in
+ warning_axioms ();
+ if is_custom r then msgnl (str "(** User defined extraction *)");
+ print_one_decl struc (modpath_of_r r) d;
+ reset ()
| _ -> assert false
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 79aeea33..4e2904ba 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: mlutil.ml 10329 2007-11-21 21:21:36Z letouzey $ i*)
+(*i $Id: mlutil.ml 13202 2010-06-25 22:36:30Z letouzey $ i*)
(*i*)
open Pp
@@ -578,7 +578,7 @@ let eta_red e =
if m = n then
[], f, a
else if m < n then
- snd (list_chop (n-m) ids), f, a
+ list_skipn m ids, f, a
else (* m > n *)
let a1,a2 = list_chop (m-n) a in
[], MLapp (f,a1), a2
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index 6dc0d5bf..14bf7cf8 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: recdef.ml 11671 2008-12-12 12:43:03Z herbelin $ *)
+(* $Id: recdef.ml 12221 2009-07-04 21:53:12Z jforest $ *)
open Term
open Termops
@@ -960,11 +960,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
let ids' = pf_ids_of_hyps g in
lid := List.rev (list_subtract ids' ids);
if !lid = [] then lid := [hid];
-(* list_iter_i *)
-(* (fun i v -> *)
-(* msgnl (str "hyp" ++ int i ++ str " " ++ *)
-(* Nameops.pr_id v ++ fnl () ++ fnl())) *)
-(* !lid; *)
tclIDTAC g
)
g
@@ -976,9 +971,22 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
Auto.h_auto None [] (Some []) g
| _ ->
incr h_num;
- tclTHEN
- (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
- e_assumption
+ (observe_tac "finishing using"
+ (
+ tclCOMPLETE(
+ tclFIRST[
+ tclTHEN
+ (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings))
+ e_assumption;
+ Eauto.eauto_with_bases
+ false
+ (true,5)
+ [delayed_force refl_equal]
+ [Auto.Hint_db.empty empty_transparent_state false]
+ ]
+ )
+ )
+ )
g)
;
Command.save_named opacity;
diff --git a/contrib/xml/xml.ml4 b/contrib/xml/xml.ml4
index e2d04cb7..5b217119 100644
--- a/contrib/xml/xml.ml4
+++ b/contrib/xml/xml.ml4
@@ -70,7 +70,7 @@ let pp strm fn =
let ch = open_out filename in
pp_ch strm ch;
close_out ch ;
- print_string ("\nWriting on file \"" ^ filename ^ "\" was succesful\n");
+ print_string ("\nWriting on file \"" ^ filename ^ "\" was successful\n");
flush stdout
| None ->
pp_ch strm stdout
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 1ae18661..f4719594 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -662,21 +662,21 @@ let _ =
| Some fn ->
let ch = open_out (fn ^ ".v") in
Buffer.output_buffer ch theory_buffer ;
+ close_out ch;
+ (* dummy glob file *)
+ let ch = open_out (fn ^ ".glob") in
close_out ch
end ;
Option.iter
(fun fn ->
let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) in
let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
- let dir = Option.get xml_library_root in
let command cmd =
if Sys.command cmd <> 0 then
Util.anomaly ("Error executing \"" ^ cmd ^ "\"")
in
- command (coqdoc^options^" -d "^dir^" "^fn^".v");
- let dot = if fn.[0]='/' then "." else "" in
- command ("mv "^dir^"/"^dot^"*.html "^fn^".xml ");
- command ("rm "^fn^".v");
+ command (coqdoc^options^" -o "^fn^".xml "^fn^".v");
+ command ("rm "^fn^".v "^fn^".glob");
print_string("\nWriting on file \"" ^ fn ^ ".xml\" was successful\n"))
ofn)
;;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 05:40:06 +0000