Commit b4e3f2ea authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

sk fk version of interactive loop

parent 26a7a9f7
true: use_menhir, explain
true: bin_annot
\ No newline at end of file
true: bin_annot
true: debug
\ No newline at end of file
......@@ -7,12 +7,28 @@ open Axiom_result
open Axiom
open Side
(*****************************)
(* Continuation Combinations *)
(*****************************)
type 'a fk = unit -> 'a
type ('a,'b) sk = 'a -> 'b fk -> 'b
(* type action_handler = *)
(* string -> state -> (state,state) sk -> state fk -> state *)
type ('a,'b,'c) t = 'a -> ('b,'c) sk -> 'c fk -> 'c
let tact_wrap : ('a -> 'b) -> ('a,'b,'c) t =
fun f v sk fk -> sk (f v) fk
let tact_return : ('a,'b,'c) t -> 'a -> 'c = fun a v ->
a v (fun r fk' -> r) (fun _ -> assert false)
let tact_andthen a b sk fk v =
a v (fun v fk' -> b v sk fk') fk
let tact_or a b sk fk =
a sk (fun () -> b sk fk)
(*************************)
......@@ -477,7 +493,7 @@ let weakly_normalize_proof ?collect:(c=false) state =
(* We apply FA everywhere we can, except for the following function symbols:
EQ, pk, sk, enc, dec
Also, we apply dup at then end. *)
let rec auto_function_application state =
let rec auto_function_application state (sk : (state,'a) sk) fk =
let goal = state.c_proof.goal in
let env = goal.env
and protected_symbols =
......@@ -566,9 +582,9 @@ let rec auto_function_application state =
let new_goal = state''.c_proof.goal in
if new_goal <> goal then
auto_function_application state''
auto_function_application state'' sk fk
else
state''
sk state'' fk
(* Automatically simplify the goal (to be called after each user input):
- weakly normalize all the terms.
......@@ -579,20 +595,18 @@ let rec auto_function_application state =
binding tables. *)
let simplify ?collect:(c=false) state =
weakly_normalize_proof ~collect:c state
|> auto_function_application
|> tact_return auto_function_application
|> apply_dup
|> apply_unitary_and_set_feedback CCA
|> fst
exception Proof_finished
exception Proof_done
exception Proof_failed
let next_goal state =
match state.danglings with
| [] ->
state.finished <- true;
raise Proof_finished
raise Proof_done
| h :: t ->
state.danglings <- t;
......@@ -604,38 +618,32 @@ let next_goal state =
goal. *)
let pre_treatment state =
let rec aux state i =
let state = simplify state in
let state =
if state.c_proof.back_track = Root then
begin
let open Fmt in
let ident ppf s = pf ppf "%s" s in
let kw style = (styled style ident) in
let auto_ift_if_root state =
if state.c_proof.back_track = Root then
let ident ppf s = Fmt.pf ppf "@[%s@]" s in
Fmt.(pf stderr "%a\n%!" (styled `Red ident) "IFT Rule applications\n%!");
pf stderr "%a\n%!" (kw `Red) "IFT Rule applications\n%!";
auto_ift state
|> simplify
end
else
state in
auto_ift state
|> simplify
else
state in
let (state, bool_res) =
apply_unitary_and_set_feedback ~print:true CCA state in
let rec prove_trivial state i =
simplify state
|> auto_ift_if_root
|> (fun state ->
let (state, bool_res) =
apply_unitary_and_set_feedback ~print:true CCA state in
let state = new_screen state in
let state = new_screen state in
if bool_res then
begin
state.c_proof.premises <- PAxiom CCA;
aux (next_goal state) (i + 1)
end
else
(state,i) in
if bool_res then
let _ = state.c_proof.premises <- PAxiom CCA in
prove_trivial (next_goal state) (i + 1)
else
(state,i)) in
let (state,num_done_goals) = aux state 0 in
let (state,num_done_goals) = prove_trivial state 0 in
if num_done_goals <> 0 then
add_error
......@@ -649,11 +657,11 @@ let pre_treatment state =
(Printf.sprintf "Number of dangling goals: %d"
(List.length state.danglings + 1))
let goal_proved state =
next_goal state
|> pre_treatment
(*****************)
(* Extend Axioms *)
(*****************)
......@@ -1770,31 +1778,40 @@ add_new_action
(* Exec a command in some state, and tries to catch any thrown exception using
the command exception handler. *)
let exec_command state command =
let exec_cmd state command sk fk =
try
Scanf.sscanf command "%s %s@\n"
(fun name args ->
try
let action = get_action name in
action.exn_handler (action.handler args) state
tact_wrap (action.exn_handler (action.handler args)) state sk fk
with
| Not_found ->
add_error (Printf.sprintf "Action does not exists: %s" name) state
|> add_error_fun rule_short_help)
|> add_error_fun rule_short_help
|> (fun state -> sk state fk))
with
| Scanf.Scan_failure s ->
add_error (Printf.sprintf "Rule shape is wrong: %s" s) state
|> (fun state -> sk state fk)
| End_of_file ->
add_error "Rule shape is wrong, maybe you forgot an argument" state
|> (fun state -> sk state fk)
let rec exec_cmd_list l state sk fk = match l with
| [] -> sk state fk
| c :: tail -> tact_andthen
(exec_cmd state)
(exec_cmd_list tail)
sk fk c
let interactive_proof state =
let rec interactive_loop : state -> state = fun state ->
let rec interactive_loop state sk fk =
let state = simplify ~collect:true state
|> new_screen in
......@@ -1803,39 +1820,39 @@ let interactive_proof state =
to it. *)
set_user_node state.c_proof;
try
(* Get user input *)
begin
try
if state.finished then raise Proof_finished;
Printf.printf "> %!";
let input_string =
if state.param.shell_mode then
get_user_input state
else
try input_line state.param.input_channel with
| End_of_file -> raise Proof_failed in
Printf.printf "> %!";
let (state,input_commands) =
try (state, parse_input input_string) with
| Term_badly_formed s ->
( add_error
(Printf.sprintf "This term is badly formed: %s" s) state,
[] ) in
let input_string =
if state.param.shell_mode then
get_user_input state
else
input_line state.param.input_channel in
exec_cmd_list input_commands state
(fun state fk' ->
interactive_loop state sk fk') fk in
let input_commands = parse_input input_string in
try
let init_state =
apply_unitary_and_set_feedback ~print:true CCA state
|> fst
|> new_screen
|> pre_treatment in
List.fold_left exec_command state input_commands
with
| Term_badly_formed s ->
add_error (Printf.sprintf "This term is badly formed: %s" s) state
end
|> interactive_loop
let final_sk (_,b) _ =
assert false in
with
| End_of_file -> raise Proof_failed in
let rec bad_backtrack () =
interactive_loop init_state final_sk bad_backtrack in
try
ignore(
apply_unitary_and_set_feedback ~print:true CCA state
|> fst
|> new_screen
|> pre_treatment
|> interactive_loop)
interactive_loop init_state final_sk bad_backtrack
with
| Proof_finished -> Printf.printf "qed.\n"
| Proof_done -> Printf.printf "qed.\n"
| Proof_failed -> Printf.printf "Incorrect proof.\n"
......@@ -32,6 +32,7 @@ val print_rule_long : Format.formatter -> rule -> unit
val rewrite : environment -> 'a term -> 'a term -> 'b term ->
msg term list -> 'b term
(*********************)
(* Rule Applications *)
(*********************)
......
......@@ -7,7 +7,6 @@ open Proof
- error_message : Error messages to be printed at the next interactive loop.
- l_error_ref : Positions where errors occured in the current interactive
loop.
- finished : True when the proof is done.
- param: The parameters of the interactive loop state. *)
type state =
{ mutable c_proof : proof;
......@@ -15,7 +14,6 @@ type state =
mutable input_history : string list;
error_message : unit -> unit;
l_error_ref : int list;
mutable finished : bool;
param : Param.param }
......@@ -37,7 +35,6 @@ let dummy_state () =
danglings = [];
input_history = [];
error_message = (fun () -> ());
finished = false;
l_error_ref = [];
param = Param.new_emacs_param true }
......@@ -47,7 +44,6 @@ let new_state param proof_list = match proof_list with
danglings = rem_proof;
input_history = [];
error_message = (fun () -> ());
finished = false;
l_error_ref = [];
param = param }
......
......@@ -15,7 +15,6 @@ open Side
- error_message : Error messages to be printed at the next interactive loop.
- l_error_ref : Positions where errors occured in the current interactive
loop.
- finished : True when the proof is done.
- param: The parameters of the interactive loop state. *)
type state =
{ mutable c_proof : proof;
......@@ -23,7 +22,6 @@ type state =
mutable input_history : string list;
error_message : unit -> unit;
l_error_ref : int list;
mutable finished : bool;
param : Param.param }
......
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