Commit 5b53de4b authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

split interactive in two

parent 929ff27d
Pipeline #1649 passed with stage
in 2 minutes and 27 seconds
open Term
open Param
open Axiom_result
exception F_out_of_bound of int
......@@ -391,7 +390,7 @@ let hashtbl_to_list ht =
(* Colored pretty printing of the formula on stdout. *)
let print_formula formula param =
let shell_mode = param.shell_mode in
let shell_mode = param.Param.shell_mode in
next_line shell_mode;
print_separator shell_mode;
......
open Term
open Param
open Axiom_result
type term_pair =
......@@ -101,7 +100,7 @@ val clean_bindings : formula -> formula
val print_separator : bool -> unit
(* Colored pretty printing of the formula on stdout. *)
val print_formula : formula -> state_param -> unit
val print_formula : formula -> Param.param -> unit
(***************************)
......
This diff is collapsed.
......@@ -37,12 +37,12 @@ let parse_problem input_channel =
| Term_lexer.Lexer_Error i ->
let error_message =
Printf.sprintf "Term_lexer, problem: %s, %d\n"
(print_position lexbuf) i in
(State.print_position lexbuf) i in
raise (Process_badly_formed error_message);
| Term_parser.Error ->
let error_message =
Printf.sprintf "Term_parser, problem: %s \"%s\"\n"
(print_position lexbuf) (Lexing.lexeme lexbuf) in
(State.print_position lexbuf) (Lexing.lexeme lexbuf) in
raise (Process_badly_formed error_message);;
......@@ -76,12 +76,12 @@ let main_interactive () =
begin
let (_,h) = ANSITerminal.size () in
ANSITerminal.set_cursor 1 h;
new_shell_param !force_color
Param.new_shell_param !force_color
end
else if !proof_file_name <> "" then
new_proof_param !proof_file_name
Param.new_proof_param !proof_file_name
else
new_emacs_param !force_color
Param.new_emacs_param !force_color
in
let formula_list =
if !file_name = "" then
......@@ -102,7 +102,7 @@ let main_interactive () =
back_track = Root;
node_type = User })
formula_list in
ignore(interactive_proof (new_state param proof_list));;
ignore(interactive_proof (State.new_state param proof_list));;
(**********************)
......@@ -110,7 +110,7 @@ let main_interactive () =
(**********************)
(* Create and set-up a dummy state and environment for testing. *)
let test_state = dummy_state ();;
let test_state = State.dummy_state ();;
let env =
let env = test_state.c_proof.goal.env in
......@@ -205,7 +205,7 @@ let unit_test_decryption_oracle = fun () ->
let dec_5_s = "dec(g(nA,nB,C(D(),nB)),sk(kA))"
and decp_5_s = "dec(g(nA_0,nB_0,C(D(),nB_0)),sk(kA_0))" in
match parse_terms test_state
match State.parse_terms test_state
(dec_0_s ^ decp_0_s ^ dec_1_s ^ decp_1_s
^ dec_2_s ^ decp_2_s ^ dec_3_s ^ decp_3_s
^ dec_4_s ^ decp_4_s ^ dec_5_s ^ decp_5_s ) with
......@@ -259,7 +259,7 @@ let unit_test_encryption_oracle = fun () ->
and encp_4_s = "enc(kA_0,r0_0,pk(kA_0))" in
match parse_terms test_state
match State.parse_terms test_state
(enc_0_s ^ encp_0_s ^ enc_1_s ^ encp_1_s
^ enc_2_s ^ encp_2_s ^ enc_3_s ^ encp_3_s
^ enc_4_s ^ encp_4_s ) with
......
(* The parameters of the interactive loop state:
- shell_mode: if true, use the input box and history in the interactive
loop input. Set to false when used with emacs.
......@@ -8,9 +7,42 @@
IfThen rule to EQ(t,s) when s is of small size (rewriting occurrences of t
into s in the then branch).
- input_channel: channel used to receive the proof instructions *)
type state_param =
type param =
{ shell_mode : bool;
force_color : bool;
small_size_heuristic : int;
mutable input_channel : in_channel;
}
let new_emacs_param force_color =
(* Setup the formatter for Fmt.stdout and Fmt.stderr *)
if force_color then
Fmt_tty.setup_std_outputs ~style_renderer:`Ansi_tty ()
else
Fmt_tty.setup_std_outputs ();
{ shell_mode = false;
force_color = force_color;
small_size_heuristic = 1;
input_channel = stdin }
let new_proof_param proof_file_name =
let input_channel = open_in proof_file_name in
{ shell_mode = false;
force_color = true;
small_size_heuristic = 1;
input_channel = input_channel }
let new_shell_param force_color =
if force_color then
Fmt_tty.setup_std_outputs ~style_renderer:`Ansi_tty ()
else
Fmt_tty.setup_std_outputs ();
{ shell_mode = true;
force_color = force_color;
small_size_heuristic = 1;
input_channel = stdin }
This diff is collapsed.
open Term
open Proof
open Rule
open Axiom_result
open Axiom
open Side
(*********************)
(* Type declarations *)
(*********************)
(* - c_proof : The current goal.
- danglings : All the other danglings node in the proof tree.
- input_history : The user input history.
- 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;
mutable danglings : proof list;
mutable input_history : string list;
error_message : unit -> unit;
l_error_ref : int list;
mutable finished : bool;
param : Param.param }
(*****************)
(* Miscellaneous *)
(*****************)
val dummy_state : unit -> state
val new_state : Param.param -> proof list -> state
val add_error : string -> state -> state
val add_error_fun : (unit -> unit) -> state -> state
val err_reset : state -> state
(*********************)
(* Parsing Functions *)
(*********************)
val print_position : Lexing.lexbuf -> string
exception Term_badly_formed of string
(* parse_terms state s : Parse the string s as a list of terms. *)
val parse_terms : state -> string -> msg term list
(* parse_b_terms state s : Parse the string s as a list of boolean terms. *)
val parse_b_terms : state -> string -> boole term list
exception Bad_argument
(* Parse the string s as a list of int. If s is '*' then return all possible
values between 0 and (i_max - 1). *)
val parse_int_list : string -> int -> int list
(* parse_string_list s : Parse the string s as a list of string separated by
whitespace. If s '*' then return all possible values between 0 and
(i_max - 1). *)
val parse_string_list : string -> string list
(* parse_input s : Parse an input string as a list of commands. Get ride of
comments, and normalize the input by removing supernumerary whitespaces. *)
val parse_input : string -> string list
(*************************)
(* Shell Input Functions *)
(*************************)
(* get_user_input state : Get user input in shell mode. *)
val get_user_input : state -> string
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