Commit 58e124fc authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

compressed proofs

parent 65b7a967
Pipeline #1652 passed with stage
in 2 minutes and 35 seconds
......@@ -41,54 +41,56 @@ let tact_or a b sk fk =
in the formula). Moreover if two rules have the same index they are applied
in the order they had in r_and_index_list. *)
let unary_build proof r_and_index_list =
List.fold_left
(fun (prev_proof,l_fun_error,l_error) (rule,index) ->
(* We compute the offset coming from the previously applied rules. *)
let offset =
(Formula.length prev_proof.goal)
- (Formula.length proof.goal) in
try
let new_form = unary_apply prev_proof.goal rule (index + offset) in
(* Ignore the rule if the formula is unchanged. *)
if new_form <> prev_proof.goal then
begin
let new_proof =
{ goal = new_form;
premises = Dangling;
back_track = BT prev_proof;
node_type = Internal } in
prev_proof.premises <- PUnary (new_proof,index + offset,rule);
(new_proof,l_fun_error,l_error)
end
else
(prev_proof,l_fun_error,l_error)
let (new_goal,l_fun_error,l_error,i_rule_list) =
List.fold_left
(fun (goal,l_fun_error,l_error,i_rule_list) (rule,index) ->
(* We compute the offset coming from the previously applied rules. *)
let offset = (Formula.length goal) - (Formula.length proof.goal) in
with
| Rule_not_applicable -> ( prev_proof,
l_fun_error,
(index + offset) :: l_error )
try
( unary_apply goal rule (index + offset),
l_fun_error,
l_error,
(index + offset,rule) :: i_rule_list )
with
| Rule_not_applicable -> ( goal,
l_fun_error,
(index + offset) :: l_error,
i_rule_list )
| Bad_rule (s,rule) ->
let err_fun = fun () ->
Fmt.pf Fmt.stderr "@[Bad rule:@;%a@;%s@]\n@?%!"
print_rule_long rule s in
| Bad_rule (s,rule) ->
let err_fun = fun () ->
Fmt.pf Fmt.stderr "@[Bad rule:@;%a@;%s@]\n@?%!"
print_rule_long rule s in
( prev_proof,
err_fun :: l_fun_error,
(index + offset) :: l_error ))
( goal,
err_fun :: l_fun_error,
(index + offset) :: l_error,
i_rule_list ))
(proof,[],[])
(proof.goal,[],[],[])
(* We sort the list in increasing order with respect to the indices.
Therefore, we apply the rules from left to right. *)
(List.stable_sort
(fun (_,i) (_,j) -> Pervasives.compare i j)
r_and_index_list)
(* We sort the list in increasing order with respect to the indices.
Therefore, we apply the rules from left to right. *)
(List.stable_sort
(fun (_,i) (_,j) -> Pervasives.compare i j)
r_and_index_list) in
(* Ignore the rule if the formula is unchanged. *)
if new_goal <> proof.goal then
begin
let new_proof =
{ goal = new_goal;
premises = Dangling;
back_track = BT proof } in
proof.premises <- PUnary (new_proof,List.rev i_rule_list);
(new_proof,l_fun_error,l_error)
end
else
(proof,l_fun_error,l_error)
(* unary_aux state r_and_index_list:
-state: current state of the interactive loop.
-r_and_index_list: see unary_build. *)
......@@ -121,14 +123,12 @@ let binary_aux state rule l_prem r_prem sk sk' fk =
let l_proof =
{ goal = c_bind proof.goal l_prem;
premises = Dangling;
back_track = BT proof;
node_type = Internal }
back_track = BT proof }
and r_proof =
{ goal = c_bind proof.goal r_prem;
premises = Dangling;
back_track = BT proof;
node_type = Internal } in
back_track = BT proof } in
proof.premises <- PBinary (l_proof,r_proof,rule);
(l_proof,r_proof) in
......@@ -224,14 +224,14 @@ let apply_dup state =
let n_proof =
{ goal = n_goal;
premises = Dangling;
back_track = BT state.c_proof;
node_type = Internal } in
back_track = BT state.c_proof } in
state.c_proof.premises <- PUnary (n_proof, -1, Duplicate);
state.c_proof <- n_proof;
end;
state.c_proof.premises <- PUnary (n_proof, [-1, Duplicate]);
state;;
{ state with c_proof = n_proof }
end
else
state
(* apply_unitary_and_set_feedback state axiom : Try to apply the unitary axiom
'axiom' to the current goal and set the feedback result field in the
......@@ -658,12 +658,11 @@ let extend_unitary : type a. a axiom_type -> state -> state =
let n_proof =
{ goal = new_goal;
premises = Dangling;
back_track = BT state.c_proof;
node_type = Internal } in
back_track = BT state.c_proof } in
state.c_proof.premises <- PUnary (n_proof,[-1,Restr]);
state.c_proof.premises <- PUnary (n_proof,-1,Restr);
state.c_proof <- n_proof;
state;;
{state with c_proof = n_proof }
(******************************)
......@@ -1030,7 +1029,9 @@ let auto_guard state sk fk =
state in
(* We apply the auto_guard element created *)
guard_decryption_list state constr g_data_list sk fk;;
let sk' state fk = sk (simplify ~collect:true state) fk in
guard_decryption_list state constr g_data_list sk' fk;;
(* auto_intro state goal : automatically guard decryption that have missing
......@@ -1663,8 +1664,6 @@ add_c_action
let try_cca state =
let state = simplify state in
let (state,bool_res) =
apply_unitary_and_set_feedback ~print:true CCA state in
......@@ -1693,6 +1692,7 @@ add_c_action
extend_unitary CCA state
|> simplify
|> auto_intro CCA
|> simplify
else
simplify state in
......@@ -1750,13 +1750,9 @@ let rec exec_cmd_list l state sk fk = match l with
let rec interactive_loop state sk fk =
let state = simplify ~collect:true state
let state = simplify state
|> new_screen in
(* We set the current proof node to be a User node, to allow backtracking
to it. *)
set_user_node state.c_proof;
Printf.printf "> %!";
let input_string =
if state.param.shell_mode then
......
......@@ -99,8 +99,7 @@ let main_interactive () =
List.map (fun formula ->
{ goal = formula;
premises = Dangling;
back_track = Root;
node_type = User })
back_track = Root })
formula_list in
interactive_proof (List.map (State.new_state param) proof_list);;
......
......@@ -3,20 +3,17 @@ open Axiom_result
open Axiom
open Rule
type node_type = Internal | User
type proof =
{ mutable goal : formula;
mutable premises : inference;
back_track : back_proof;
mutable node_type : node_type }
back_track : back_proof }
and back_proof = BT of proof | Root
and inference =
| Dangling
| PAxiom : _ axiom_type -> inference
| PUnary of proof * int * rule
| PUnary of proof * (int * rule) list
| PBinary of proof * proof * rule
......@@ -24,75 +21,6 @@ and inference =
(* Proof Tree Navigation *)
(*************************)
let set_user_node proof = proof.node_type <- User;;
(* get_danglings proof: Get the danglings leaves from proof. *)
let get_danglings proof =
let rec aux proof acc = match proof.premises with
| Dangling -> proof :: acc
| PAxiom _ -> acc
| PUnary (n_proof,_,_) -> aux n_proof acc
| PBinary (l_proof,r_proof,_) -> aux r_proof (aux l_proof acc) in
aux proof []
(* back_track c_proof danglings: Back track one step from c_proof, and update
accordingly the list of danglings leaves. *)
let rec back_track c_proof danglings = match c_proof.back_track with
| Root -> (c_proof,danglings)
| BT father -> match father.premises with
| Dangling | PAxiom _ -> failwith "Back Tracking Error: Not Possible"
| PUnary (_,_,_) ->
if father.node_type = User then
(father,danglings)
else
back_track father danglings
| PBinary (l_proof,r_proof,_) ->
let to_remove =
if c_proof == l_proof then
get_danglings r_proof
else if c_proof == r_proof then
get_danglings l_proof
else
failwith "Back Tracking Error: badly formed proof tree" in
let new_danglings =
List.filter (fun x -> not (List.mem x to_remove)) danglings in
if father.node_type = User then
(father,new_danglings)
else
back_track father new_danglings
exception Bad_for_track
(* for_track c_proof: Go one step forward into the proof tree c_proof, and give
the new dangling leaves. *)
let for_track c_proof =
let rec aux c_proof acc = match c_proof.premises with
| Dangling | PAxiom _ -> raise Bad_for_track
| PUnary (n_proof,_,_) ->
if n_proof.node_type = User then
(n_proof,acc)
else
aux n_proof acc
| PBinary (l_proof,r_proof,_) ->
if l_proof.node_type = User then
(l_proof,r_proof :: acc)
else
aux l_proof ( r_proof :: acc ) in
aux c_proof []
let rec get_root proof = match proof.back_track with
| Root -> proof
| BT p_proof -> get_root p_proof
......@@ -116,9 +44,14 @@ let rec print_proof_latex channel proof =
print_formula_latex channel proof.goal;
fprintf channel "}\n{}";
| PUnary (n_proof, pos, rule) ->
fprintf channel "\\infer[{\\huge\\text{%s}(%d)}]{\n"
(rule_to_string rule) pos;
| PUnary (n_proof, r_list) ->
fprintf channel "\\infer[{\\huge%a}]{\n"
(fun chan list ->
List.iter (fun (pos,rule) ->
fprintf chan "\text{%s}(%d)"
(rule_to_string rule) pos)
list)
r_list;
print_formula_latex channel proof.goal;
fprintf channel "}\n{\n";
print_proof_latex channel n_proof;
......
......@@ -3,39 +3,24 @@ open Axiom_result
open Axiom
open Rule
type node_type = Internal | User
type proof =
{ mutable goal : formula;
mutable premises : inference;
back_track : back_proof;
mutable node_type : node_type }
back_track : back_proof }
and back_proof = BT of proof | Root
and inference =
| Dangling
| PAxiom : _ axiom_type -> inference
| PUnary of proof * int * rule
| PUnary of proof * (int * rule) list
| PBinary of proof * proof * rule
exception Bad_for_track
(*************************)
(* Proof Tree Navigation *)
(*************************)
val set_user_node : proof -> unit
(* back_track c_proof danglings: Back track one step from c_proof, and update
accordingly the list of danglings leaves. *)
val back_track : proof -> proof list -> proof * proof list
(* for_track c_proof: Go one step forward into the proof tree c_proof, and give
the new dangling leaves. *)
val for_track : proof -> proof * proof list
val get_root : proof -> proof
......
......@@ -2,14 +2,13 @@ open Term
open Proof
(* - 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.
- param: The parameters of the interactive loop state. *)
type state =
{ mutable c_proof : proof;
{ c_proof : proof;
mutable input_history : string list;
error_message : unit -> unit;
l_error_ref : int list;
......@@ -27,8 +26,7 @@ let dummy_state () =
let dummy_proof = { goal = dummy_formula;
premises = Dangling;
back_track = Root;
node_type = Internal } in
back_track = Root } in
{ c_proof = dummy_proof;
input_history = [];
......
......@@ -10,14 +10,13 @@ open Side
(*********************)
(* - 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.
- param: The parameters of the interactive loop state. *)
type state =
{ mutable c_proof : proof;
{ c_proof : proof;
mutable input_history : string list;
error_message : unit -> unit;
l_error_ref : int list;
......
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