124 lines
4.5 KiB
Diff
124 lines
4.5 KiB
Diff
--- ./Makefile.in.orig 2014-03-17 16:01:46.000000000 -0600
|
|
+++ ./Makefile.in 2014-06-26 12:30:00.000000000 -0600
|
|
@@ -222,7 +222,7 @@ CMO_EXPORT = src/lib.cmo src/rc.cmo src
|
|
src/effect.cmo src/pp.cmo src/option_misc.cmo \
|
|
src/parser.cmo src/lexer.cmo src/report.cmo \
|
|
src/explain.cmo \
|
|
- src/xml.cmo src/project.cmo
|
|
+ src/xml.cmo src/whyproject.cmo
|
|
|
|
CMO = src/lib.cmo src/rc.cmo tools/dpConfig.cmo \
|
|
src/version.cmo src/options.cmo src/linenum.cmo src/loc.cmo \
|
|
@@ -239,7 +239,7 @@ CMO = src/lib.cmo src/rc.cmo tools/dpCon
|
|
src/holl.cmo src/harvey.cmo src/simplify.cmo \
|
|
src/regen.cmo src/mizar.cmo src/smtlib.cmo src/coq.cmo \
|
|
src/zenon.cmo src/z3.cmo src/cvcl.cmo tools/calldp.cmo \
|
|
- src/xml.cmo src/project.cmo \
|
|
+ src/xml.cmo src/whyproject.cmo \
|
|
src/why3_kw.cmo src/why3.cmo src/pretty.cmo \
|
|
src/unionfind.cmo src/theoryreducer.cmo \
|
|
src/theory_filtering.cmo src/hypotheses_filtering.cmo \
|
|
--- ./src/options.mli.orig 2014-03-17 16:01:46.000000000 -0600
|
|
+++ ./src/options.mli 2014-06-26 12:30:00.000000000 -0600
|
|
@@ -185,7 +185,7 @@ val files : string list
|
|
(*s GUI? *)
|
|
|
|
val gui : bool ref
|
|
-val gui_project : Project.t option ref
|
|
+val gui_project : Whyproject.t option ref
|
|
val lib_files_to_load : string list
|
|
|
|
(*
|
|
--- ./src/pretty.ml.orig 2014-03-17 16:01:46.000000000 -0600
|
|
+++ ./src/pretty.ml 2014-06-26 12:30:00.000000000 -0600
|
|
@@ -415,12 +415,12 @@ let output_project f =
|
|
with Not_found ->
|
|
functions := SMap.add fn SMap.empty !functions)
|
|
Util.program_locs ;
|
|
- let p = Project.create (Filename.basename f) in
|
|
- Project.set_project_context_file p (f ^ "_ctx.why");
|
|
+ let p = Whyproject.create (Filename.basename f) in
|
|
+ Whyproject.set_project_context_file p (f ^ "_ctx.why");
|
|
List.iter
|
|
(fun (expl,fpo) ->
|
|
let n = expl.lemma_or_fun_name in
|
|
- let _ = Project.add_lemma p n expl fpo in ())
|
|
+ let _ = Whyproject.add_lemma p n expl fpo in ())
|
|
!lemmas;
|
|
SMap.iter
|
|
(fun fname behs ->
|
|
@@ -430,15 +430,15 @@ let output_project f =
|
|
floc
|
|
with Not_found -> Loc.dummy_floc
|
|
in
|
|
- let f = Project.add_function p fname floc in
|
|
+ let f = Whyproject.add_function p fname floc in
|
|
SMap.iter
|
|
(fun beh vcs ->
|
|
- let be = Project.add_behavior f beh floc in
|
|
+ let be = Whyproject.add_behavior f beh floc in
|
|
List.iter
|
|
(fun (expl,fpo) ->
|
|
- let _ = Project.add_goal be expl fpo in ())
|
|
+ let _ = Whyproject.add_goal be expl fpo in ())
|
|
vcs)
|
|
behs)
|
|
!functions;
|
|
- Project.save p f;
|
|
+ Whyproject.save p f;
|
|
p
|
|
--- ./src/pretty.mli.orig 2014-03-17 16:01:46.000000000 -0600
|
|
+++ ./src/pretty.mli 2014-06-26 12:30:00.000000000 -0600
|
|
@@ -51,4 +51,4 @@ val output_files : string -> unit
|
|
(* [output_project f] produces a whole project description, in a file
|
|
[f.wpr], together with other needed files [f_ctx.why], [f_lemmas.why],
|
|
and each goal in a separate file [f_po<i>.why] for i=1,2,... *)
|
|
-val output_project : string -> Project.t
|
|
+val output_project : string -> Whyproject.t
|
|
--- ./src/whyweb.ml.orig 2014-03-17 16:01:46.000000000 -0600
|
|
+++ ./src/whyweb.ml 2014-06-26 12:30:00.000000000 -0600
|
|
@@ -30,7 +30,7 @@
|
|
(**************************************************************************)
|
|
|
|
open Format
|
|
-open Project
|
|
+open Whyproject
|
|
|
|
(*prover*)
|
|
let provers = [Ergo ; Simplify ; Z3 ; Yices ; Cvc3]
|
|
@@ -169,7 +169,7 @@ let file = match !file with
|
|
| None -> ()
|
|
| Some f -> Arg.usage spec usage; exit 1
|
|
|
|
-let proj = ref (Project.create "")
|
|
+let proj = ref (Whyproject.create "")
|
|
|
|
let proj_file = ref ""
|
|
|
|
@@ -261,7 +261,7 @@ let interp_com c =
|
|
let _ = Thread.create (launch_behavior Cvc3) b in ()
|
|
| `LaunchCvc3Function f ->
|
|
let _ = Thread.create (launch_function Cvc3) f in ()
|
|
- | `Save -> Project.save !proj !proj.project_name
|
|
+ | `Save -> Whyroject.save !proj !proj.project_name
|
|
end;
|
|
loc
|
|
with Not_found -> ("",0,0,0)
|
|
@@ -344,7 +344,7 @@ let main_page msg =
|
|
let load_prj file =
|
|
eprintf "Reading file %s@." file;
|
|
try
|
|
- proj := Project.load file;
|
|
+ proj := Whyproject.load file;
|
|
proj_file := file;
|
|
with
|
|
Sys_error _ ->
|
|
@@ -527,7 +527,7 @@ wprint "<center><a href=\"%s\">Save Proj
|
|
<table border=\"1\" cellpadding=\"0\" cellspacing=\"0\">" ns;
|
|
wprint "<tr><th></th>";
|
|
List.iter (fun prover ->
|
|
- wprint "<th>%s</th>" (Project.provers_name prover))
|
|
+ wprint "<th>%s</th>" (Whyproject.provers_name prover))
|
|
provers;
|
|
wprint "</tr>
|
|
";
|