Commit 5e5163b6 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

ITP: access to strategies

parent 9f5a5517
......@@ -13,3 +13,4 @@ exception SyntaxError of string
val parse : 'a Session.env_session -> string -> Strategy.t
val parse2 : Env.env -> Whyconf.config -> string -> Strategy.t
......@@ -10,7 +10,6 @@
(********************************************************************)
{
open Session
open Strategy
exception SyntaxError of string
......@@ -28,17 +27,19 @@
}
type 'a code = {
env: 'a Session.env_session;
env: Env.env;
whyconf: Whyconf.config;
mutable instr: instruction array;
mutable next: int;
labels: (string, label) Hashtbl.t; (* label name -> label *)
mutable temp: int;
}
let create_code env =
let create_code env conf =
let h = Hashtbl.create 17 in
Hashtbl.add h "exit" { defined = Some (-1); temporary = 0 };
{ env = env;
whyconf = conf;
instr = Array.make 10 (Igoto 0);
next = 0;
temp = 1;
......@@ -80,7 +81,7 @@
let prover code p =
try
let fp = Whyconf.parse_filter_prover p in
Whyconf.filter_one_prover code.env.whyconf fp
Whyconf.filter_one_prover code.whyconf fp
with
| Whyconf.ProverNotFound _ ->
error "Prover %S not installed or not configured" p
......@@ -93,10 +94,10 @@
let transform code t =
try
ignore (Trans.lookup_transform t code.env.Session.env)
ignore (Trans.lookup_transform t code.env)
with Trans.UnknownTrans _ ->
try
ignore (Trans.lookup_transform_l t code.env.Session.env)
ignore (Trans.lookup_transform_l t code.env)
with Trans.UnknownTrans _->
error "transformation %S is unknown" t
......@@ -140,7 +141,21 @@ rule scan code = parse
{
let parse env s =
let parse2 env conf s =
let code = create_code env conf in
scan code (Lexing.from_string s);
let label = Array.make code.temp 0 in
let fill name lab = match lab.defined with
| None -> error "label '%s' is undefined" name
| Some n -> label.(lab.temporary) <- n in
Hashtbl.iter fill code.labels;
let solve = function
| Icall_prover _ as i -> i
| Itransform (t, n) -> Itransform (t, label.(n))
| Igoto n -> Igoto label.(n) in
Array.map solve (Array.sub code.instr 0 code.next)
(*
let code = create_code env in
scan code (Lexing.from_string s);
let label = Array.make code.temp 0 in
......@@ -153,5 +168,8 @@ rule scan code = parse
| Itransform (t, n) -> Itransform (t, label.(n))
| Igoto n -> Igoto label.(n) in
Array.map solve (Array.sub code.instr 0 code.next)
*)
let parse env s = parse2 env.Session.env env.Session.whyconf s
}
......@@ -23,9 +23,11 @@ let type_ptree ~as_fmla t task =
Ident.Mid.fold
(fun _id th acc ->
let name = th.Theory.th_name in
(**)
Format.eprintf "[Args_wrapper.type_ptree] use theory %s (%s)@."
_id.Ident.id_string
name.Ident.id_string;
(**)
Theory.close_namespace
(Theory.use_export
(Theory.open_namespace acc name.Ident.id_string)
......@@ -35,7 +37,12 @@ let type_ptree ~as_fmla t task =
in
let th_uc =
List.fold_left
(fun acc d -> Theory.add_decl ~warn:false acc d)
(fun acc d ->
(**)
Format.eprintf "[Args_wrapper.type_ptree] add decl %a@."
Pretty.print_decl d;
(**)
Theory.add_decl ~warn:false acc d)
th_uc local_decls
in
if as_fmla
......
......@@ -452,8 +452,8 @@ let test_print_goal fmt _args =
let id = nearest_goal () in
let task = Session_itp.get_task cont.Controller_itp.controller_session id in
fprintf fmt "@[====================== Task =====================@\n%a@]@."
(*(fprintf fmt "@[%a@]@?" Pretty.print_task task)*) Pretty.print_task
(*Driver.print_task ~cntexample:false task_driver)*) task
(* (fprintf fmt "@[%a@]@?" Pretty.print_task task) Pretty.print_task *)
(Driver.print_task ~cntexample:false task_driver) task
let test_save_session _fmt args =
match args with
......@@ -483,11 +483,52 @@ let test_transform_and_display fmt args =
C.schedule_transformation cont id tr tl ~callback
| _ -> printf "Error: Give the name of the transformation@."
(***************** strategy *****************)
let loaded_strategies = ref []
let strategies () =
match !loaded_strategies with
| [] ->
let strategies = Whyconf.get_strategies config in
let strategies =
Stdlib.Mstr.fold_left
(fun acc _ st ->
let name = st.Whyconf.strategy_name in
try
let code = st.Whyconf.strategy_code in
let code = Strategy_parser.parse2 env config code in
let shortcut = st.Whyconf.strategy_shortcut in
Format.eprintf "[Why3shell] Strategy '%s' loaded.@." name;
(name, shortcut, st.Whyconf.strategy_desc, code) :: acc
with Strategy_parser.SyntaxError msg ->
Format.eprintf
"[Why3shell warning] Loading strategy '%s' failed: %s@." name msg;
acc)
[]
strategies
in
let strategies = List.rev strategies in
loaded_strategies := strategies;
strategies
| l -> l
let list_strategies _fmt _args =
let l = strategies () in
let pp_strat fmt (n,s,_,_) = fprintf fmt "%s: %s" s n in
printf "@[<hov 2>== Known strategies ==@\n%a@]@."
(Pp.print_list Pp.newline pp_strat) l
(*******)
let commands =
[
"list-provers", "list available provers", list_provers;
"list-transforms", "list available transformations", list_transforms;
"list-strategies", "list available strategies", list_strategies;
"a", "<transname> <args>: apply the transformation <transname> with arguments <args>", apply_transform;
"b", "<transname> <args>: behave like a but add function to display into the callback", test_transform_and_display;
"p", "print the session in raw form", dump_session_raw;
......
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