Commit 974e3a35 authored by MARCHE Claude's avatar MARCHE Claude

whyrc

parent 1620f2f8
......@@ -125,8 +125,7 @@ TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
DRIVER_CMO := driver_ast.cmo call_provers.cmo dynlink_compat.cmo \
driver_parser.cmo\
driver_lexer.cmo driver.cmo
driver_parser.cmo driver_lexer.cmo whyrc.cmo driver.cmo
DRIVER_CMO := $(addprefix src/driver/,$(DRIVER_CMO))
PRINTER_CMO := print_real.cmo alt_ergo.cmo why3.cmo smt.cmo coq.cmo
......@@ -244,10 +243,10 @@ $(ORM_CMO): INCLUDES=-I src/orm -I +sqlite3
src/manager/orm_schema.ml: $(ORM_CMO)
MANAGER_CMO := db.cmo
MANAGER_CMO := db.cmo test.cmo
MANAGER_CMO := $(addprefix src/manager/,$(MANAGER_CMO))
$(MANAGER_CMO): INCLUDES=-I src/core -I src/driver -I src/manager -I +sqlite3 -I +threads
$(MANAGER_CMO): INCLUDES=-I src/manager -I +sqlite3 -I +threads
$(MANAGER_CMO): $(LIBCMI)
bin/manager.byte: $(LIBCMA) $(MANAGER_CMO)
......
let default_why3rc_file () =
let home =
try Sys.getenv "HOME"
with Not_found ->
(* try windows env var *)
try Sys.getenv "USERPROFILE"
with Not_found -> ""
in
Filename.concat (Filename.concat home ".why") "why3rc"
let read_config_file ?(name = default_why3rc_file()) =
assert false (* TODO *)
let known_provers () =
assert false (* TODO *)
let get_driver name env =
assert false (* TODO *)
let add_driver_config id file cmd =
assert false (* TODO *)
let save () =
assert false (* TODO *)
(** {2 access to user configuration and drivers} *)
val read_config_file: ?name:string -> unit
(** reads the config file from file [name]. The
default rc file name is "$HOME/.why/why3rc" if HOME is set, or
"$USERPROFILE/.why/why3rc" if USERPROFILE is set, or "./.why/why3rc"
otherwise *)
val known_provers: unit -> string list
(** returns the list of known prover ids. *)
val get_driver: string -> Env.env -> Driver.driver
(** returns the driver associated to the given prover id *)
(** {2 configuration update} *)
val add_driver_config: string -> string -> string -> unit
(** [add_driver_config id file cmd] adds in the current configuration
a new prover named [id], associated to a new driver description
file built from the template [file] and the command line [cmd].
This new setting is recorded in the user's rc file when [save] is called.
{!add_driver_config} *)
val save : unit -> unit
(** saves the current configuration into the same file as given in
[read_config_file] *)
......@@ -197,7 +197,7 @@ let print_th_namespace fmt th =
let fname_printer = ref (Ident.create_ident_printer [])
let do_task env drv fname tname th task =
let do_task env drv fname tname (th : Why.Theory.theory) (task : Task.task) =
if !opt_prove then begin
let res = Driver.call_prover ~debug:!opt_debug ?timeout drv task in
printf "%s %s %s : %a@." fname tname
......
......@@ -111,7 +111,7 @@ type proof_attempt_status =
type prover_data =
{ prover_name : string;
driver : Driver.driver;
driver : Why.Driver.driver;
}
type external_proof = {
......@@ -134,7 +134,7 @@ let trace e = e.trace
let proof_obsolete e = e.proof_obsolete
type goal_origin =
| Goal of Decl.prsymbol
| Goal of Why.Decl.prsymbol
(*
| VCfun of loc * explain * ...
| Subgoal of goal
......@@ -142,13 +142,13 @@ type goal_origin =
type transf_data =
{ transf_name : string;
transf_action : Task.task Register.tlist_reg
transf_action : Why.Task.task Why.Register.tlist_reg
}
type goal = {
mutable id : db_ident option;
mutable task : Task.task;
mutable goal_id : db_ident option;
mutable task : Why.Task.task;
mutable task_checksum: string;
(*
mutable parent : transf option;
......@@ -588,6 +588,13 @@ end
module Goal = struct
type t = goal
let hash g = Hashtbl.hash g.goal_id
let equal g1 g2 = g1.goal_id = g2.goal_id
let compare g1 g2 = Pervasives.compare g1.goal_id g2.goal_id
(*
let init db =
......@@ -1019,19 +1026,27 @@ end
let init_db ?(busyfn=default_busyfn) ?(mode=Immediate) db_name =
match !current_db with
| None ->
current_db <- Some {
let db = {
raw_db = Sqlite3.db_open db_name;
in_transaction = 0;
mode = mode;
busyfn = busyfn }
busyfn = busyfn;
}
in
current_db := Some db;
Loc.init db;
(*
External_proof.init db;
Goal.init db;
Transf.init db;
*)
db
| Some _ -> failwith "database already opened"
let init_base f = init_db f
let root_goals () = assert false (* TODO *)
exception AlreadyAttempted
......@@ -1042,7 +1057,7 @@ let try_prover ~timelimit:int ?memlimit:int (g : goal) (d: prover_data) : unit =
let add_transformation (g : goal) (t : transf) : unit =
assert false (* TODO *)
let add_or_replace_goal (g : goal) : unit =
let add_or_replace_task (name : string) (t : Why.Task.task) : unit =
assert false (* TODO *)
let read_db_from_file (file : string) : goal list =
......
......@@ -64,7 +64,7 @@ type proof_attempt_status =
type prover_data =
{ prover_name : string;
driver : Driver.driver;
driver : Why.Driver.driver;
}
type external_proof
......@@ -86,16 +86,30 @@ type goal_origin =
*)
*)
type goal
module Goal : sig
type t = goal
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
end
type transf_data =
{ transf_name : string;
transf_action : Task.task Register.tlist_reg
transf_action : Why.Task.task Why.Register.tlist_reg
}
type transf
type goal
(** goal accessors *)
val goal_task : goal -> Task.task
val goal_task : goal -> Why.Task.task
val goal_task_checksum: goal -> string
(*
val parent : goal -> transf option
......@@ -115,11 +129,14 @@ val goal_proved : goal -> bool
(** transf accessors *)
val transf_data : transf -> transf_data
val transf_obsolete : transf -> bool
val subgoals : transf -> goal list
(** {2 The persistent database} *)
val init_base : string -> unit
......@@ -130,6 +147,7 @@ val root_goals : unit -> goal list
(** {2 attempts to solve goals} *)
exception AlreadyAttempted
......@@ -184,7 +202,7 @@ val add_transformation: goal -> transf -> unit
(* {2 goal updates} *)
val add_or_replace_goal: goal -> unit
val add_or_replace_task: string -> Why.Task.task -> unit
(** updates the database with the new goal. If a goal with the same
origin already exists, it is checked whether the task to
prove is different or not. If it is the same, proof attempts are
......
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