Commit 6d2c226d authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

started to do a huge rework of the way environement are handled, with the...

started to do a huge rework of the way environement are handled, with the ultimate goal of using a functional implementation of environements
parent deb4468e
Pipeline #1642 passed with stage
in 2 minutes and 40 seconds
......@@ -19,9 +19,9 @@ let Outcome v1 v2 v3 sk =
let res1 = dec(v1,sk) in
let res2 = dec(v2,sk) in
let res3 = dec(v3,sk) in
let acount = count(A(),res1,res2,res3) in
let account = count(A(),res1,res2,res3) in
let bcount = count(B(),res1,res2,res3) in
out(cres,<acount,bcount>);
out(cres,<account,bcount>);
let SubTally{i} v1 v2 v3 bv1 bv2 pks1 pks2 pks3 sk =
......
......@@ -48,51 +48,6 @@ let update_unitary_result element result =
hidden_status = element.hidden_status;
unitary_result = result }
exception No_such_binding of variable_string
(* Replace a variable by a name if it is binded in the environement. This is
used after parsing a term, to disambiguate between variable and names.
Raise No_such_binding is a binding does not exist. *)
let rec set_binded_names : type a. formula -> a term -> a term =
fun formula term -> match term with
| Bot -> term
| True -> term
| False -> term
| Name _ -> term
| Var (s,Msg) ->
if is_binded formula.env s then
let s_type = Hashtbl.find formula.env.string_types s in
if s_type = TName then
Name (s,Msg)
else
term
else
raise (No_such_binding s)
| Var (s,Bool) ->
if is_binded formula.env s then
let s_type = Hashtbl.find formula.env.string_types s in
if s_type = BTName then
Name (s,Bool)
else
term
else term
| Fun (s, l) ->
Fun (s, List.map (set_binded_names formula) l)
| If (b, u, v) ->
If ( set_binded_names formula b,
set_binded_names formula u,
set_binded_names formula v )
| EQ (u, v) ->
EQ ( set_binded_names formula u,
set_binded_names formula v )
let type_check_formula_element_list env formula_element_list =
......@@ -282,10 +237,6 @@ let reveal_element formula i =
(* Binders Handling *)
(********************)
(* Raised when a binding has the wrong type. The first type is the wanted type
and the second is the already existing type. *)
exception Bad_binding of string_type * string_type
let size_t_bindings formula = Hashtbl.length formula.env.t_bindings
let size_bt_bindings formula = Hashtbl.length formula.env.bt_bindings
......@@ -293,104 +244,26 @@ let size_bt_bindings formula = Hashtbl.length formula.env.bt_bindings
let size_bindings formula =
(size_t_bindings formula) + (size_bt_bindings formula)
(* Give the default behaviour when adding a binding. Should be over-ridden by
the state Param values. *)
let default_collect = ref true;;
(* Set the value of the global variable default_collect. *)
let new_default_collect bool = default_collect := bool
(* add_t_binding formula ~collect:collect s t: Add a new binding between the
term variable s and the term t in formula. The term t must type-check. If
the optional argument collect is true then collect all bindings in t before
adding it. *)
let add_t_binding formula ?(collect = !default_collect) s t =
type_check formula.env t;
let t = if collect then collect_all formula.env t else t in
if Hashtbl.mem formula.env.string_types s then
raise (Bad_binding (TVar,(Hashtbl.find formula.env.string_types s)))
else
begin
let env' = copy_env formula.env in
Hashtbl.add env'.string_types s TVar;
Hashtbl.filter_map_inplace
(fun _ u -> Some (collect_var u s t))
env'.t_bindings;
Hashtbl.filter_map_inplace
(fun _ bu -> Some (collect_var bu s t))
env'.bt_bindings;
Hashtbl.add env'.t_bindings s t;
Hashtbl.add env'.hide_bindings s true;
let f' = List.map (fun entry ->
match entry.term_pair with
| T (u,v) ->
update_term_pair entry (T ( collect_var u s t,
collect_var v s t ))
| B (bu,bv) ->
update_term_pair entry (B ( collect_var bu s t,
collect_var bv s t )))
formula.formula_element_list in
{ formula_element_list = f';
env = env' }
end
(* add_bt_binding formula ~collect:collect s t: Add a new binding between the
boolean term variable s and the boolean term bt in formula. The term bt must
type-check. If the optional argument collect is true then collect all
bindings in bt before adding it. *)
let add_bt_binding formula ?(collect = !default_collect) s bt =
type_check formula.env bt;
let bt = if collect then collect_all formula.env bt else bt in
if Hashtbl.mem formula.env.string_types s then
raise (Bad_binding (BTVar,(Hashtbl.find formula.env.string_types s)))
else
begin
let env' = copy_env formula.env in
Hashtbl.add env'.string_types s BTVar;
Hashtbl.filter_map_inplace
(fun _ u -> Some (collect_bvar u s bt))
env'.t_bindings;
Hashtbl.filter_map_inplace
(fun _ bu -> Some (collect_bvar bu s bt))
env'.bt_bindings;
Hashtbl.add env'.bt_bindings s bt;
Hashtbl.add env'.hide_bindings s true;
let f' = List.map (fun entry ->
match entry.term_pair with
| T (u,v) ->
update_term_pair entry (T ( collect_bvar u s bt,
collect_bvar v s bt ))
(* add_binding formula s t: Add a new binding between the term variable s
and the term t in formula. The term t must type-check. *)
let add_binding : type a. formula -> variable_string -> a term -> formula =
fun formula s t ->
let env' = env_add_binding formula.env s t in
| B (bu,bv) ->
update_term_pair entry (B ( collect_bvar bu s bt,
collect_bvar bv s bt )))
let f' = List.map (fun entry ->
match entry.term_pair with
| T (u,v) ->
update_term_pair entry (T ( collect_var u s t,
collect_var v s t ))
formula.formula_element_list in
| B (bu,bv) ->
update_term_pair entry (B ( collect_var bu s t,
collect_var bv s t )))
{ formula_element_list = f';
env = env' }
end
formula.formula_element_list in
{ formula_element_list = f';
env = env' }
(* remove_binding formula s: Remove the binding associated with s in formula. *)
let remove_binding formula s =
......@@ -503,53 +376,6 @@ let clean_bindings formula =
clean_bindings_aux Msg formula
|> (clean_bindings_aux Bool)
(* hide_binding formula s: Hide the binding associated with s in formula. *)
let hide_binding formula s =
if Hashtbl.mem formula.env.t_bindings s then
begin
(* Sanity Check *)
assert (Hashtbl.find formula.env.string_types s = TVar);
Hashtbl.replace formula.env.hide_bindings s true
end
else if Hashtbl.mem formula.env.bt_bindings s then
begin
(* Sanity Check *)
assert (Hashtbl.find formula.env.string_types s = BTVar);
Hashtbl.replace formula.env.hide_bindings s true
end
else
raise (No_such_binding s)
let hide_all_bindings formula =
Hashtbl.filter_map_inplace
(fun s _ -> Some true)
formula.env.hide_bindings;;
(* reveal_binding formula s: Reveal the binding associated with s in formula. *)
let reveal_binding formula s =
if Hashtbl.mem formula.env.t_bindings s then
begin
(* Sanity Check *)
assert (Hashtbl.find formula.env.string_types s = TVar);
Hashtbl.replace formula.env.hide_bindings s false
end
else if Hashtbl.mem formula.env.bt_bindings s then
begin
(* Sanity Check *)
assert (Hashtbl.find formula.env.string_types s = BTVar);
Hashtbl.replace formula.env.hide_bindings s false
end
else
raise (No_such_binding s)
let reveal_all_bindings formula =
Hashtbl.filter_map_inplace
(fun s _ -> Some false)
formula.env.hide_bindings;;
(*******************)
......
......@@ -31,11 +31,6 @@ val get_msg_term_pair : term_pair -> msg term * msg term
val update_unitary_result : formula_element -> axiom_result -> formula_element
(* Replace a variable by a name if it is binded in the environement. This is
used after parsing a term, to disambiguate between variable and names.
Raise No_such_binding is a binding does not exist. *)
val set_binded_names : formula -> 'a term -> 'a term
(* new formula ~env:env l l': Create a new formula whose boolean elements are
the element of l and term elements are the elements of l'. A type checking
is perfomed before creating the formula *)
......@@ -87,46 +82,16 @@ val reveal_element : formula -> int -> formula
(* Binders Handling *)
(********************)
(* Raised when a binding has the wrong type. The first type is the wanted type
and the second is the already existing type. *)
exception Bad_binding of string_type * string_type
exception No_such_binding of variable_string
(* Set the value of the global variable default_collect. *)
val new_default_collect : bool -> unit
(* add_t_binding formula ~collect:collect s t: Add a new binding between the
term variable s and the term t in formula. The term t must type-check. If
the optional argument collect is true then collect all bindings in t before
adding it. *)
val add_t_binding :
formula -> ?collect:bool -> variable_string -> msg term -> formula
(* add_bt_binding formula ~collect:collect s t: Add a new binding between the
boolean term variable s and the boolean term bt in formula. The term bt must
type-check. If the optional argument collect is true then collect all
bindings in bt before adding it. *)
val add_bt_binding :
formula -> ?collect:bool -> variable_string -> boole term -> formula
(* add_binding formula s t: Add a new binding between the term variable s
and the term t in formula. The term t must type-check. *)
val add_binding : formula -> variable_string -> 'a term -> formula
(* remove_binding formula s: Remove the binding associated with s in formula. *)
val remove_binding : formula -> variable_string -> formula
(* clean_bindings formula : Remove all bindings that are unused. *)
val clean_bindings : formula -> formula
(* hide_binding formula s: Hide the binding associated with s in formula. *)
val hide_binding : formula -> variable_string -> unit
val hide_all_bindings : formula -> unit
(* reveal_binding formula s: Reveal the binding associated with s in formula. *)
val reveal_binding : formula -> variable_string -> unit
val reveal_all_bindings : formula -> unit
(*******************)
(* Pretty Printing *)
......
......@@ -34,9 +34,6 @@ type interactive_state =
param : state_param }
let new_emacs_param force_color =
let default_collect = true in
Formula.new_default_collect default_collect;
(* Setup the formatter for Fmt.stdout and Fmt.stderr *)
if force_color then
......@@ -45,37 +42,26 @@ let new_emacs_param force_color =
Fmt_tty.setup_std_outputs ();
{ shell_mode = false;
default_collect = default_collect;
force_color = force_color;
small_size_heuristic = 1;
input_channel = stdin }
let new_proof_param proof_file_name =
let default_collect = true in
Formula.new_default_collect default_collect;
let input_channel = open_in proof_file_name in
{ shell_mode = false;
default_collect = default_collect;
force_color = true;
small_size_heuristic = 1;
input_channel = input_channel }
let new_shell_param force_color =
let default_collect = true in
Formula.new_default_collect default_collect;
if force_color then
Fmt_tty.setup_std_outputs ~style_renderer:`Ansi_tty ()
else
Fmt_tty.setup_std_outputs ();
{ shell_mode = true;
default_collect = default_collect;
force_color = force_color;
small_size_heuristic = 1;
input_channel = stdin }
......@@ -159,7 +145,7 @@ let parse_terms state s =
Printf.eprintf "\n%!")
l_res) in
List.map (set_binded_names state.c_proof.goal) l_res
List.map (set_binded_names state.c_proof.goal.env) l_res
with
| Term_lexer.Lexer_Error (i) ->
......@@ -199,7 +185,7 @@ let parse_b_terms state s =
Printf.eprintf "\n%!")
l_res) in
List.map (set_binded_names state.c_proof.goal) l_res
List.map (set_binded_names state.c_proof.goal.env) l_res
with
| Term_lexer.Lexer_Error i ->
......@@ -677,7 +663,7 @@ let binding_aux state y =
| Scan_failure _ ->
sscanf y "%s = %s@!" (fun name u ->
try match parse_terms state u with
| [t_u] -> add_t_binding state.c_proof.goal name t_u
| [t_u] -> add_binding state.c_proof.goal name t_u
| l ->
let error_message =
sprintf
......@@ -689,7 +675,7 @@ let binding_aux state y =
with
| Term_badly_formed _ ->
match parse_b_terms state u with
| [b_a] -> add_bt_binding state.c_proof.goal name b_a
| [b_a] -> add_binding state.c_proof.goal name b_a
| l ->
let error_message =
sprintf
......@@ -1295,11 +1281,11 @@ add_new_action
| Scanf.Scan_failure _ ->
sscanf y "bind %s@!" (fun z ->
if z = "*" then
hide_all_bindings state.c_proof.goal
hide_all_bindings state.c_proof.goal.env
else
let l_s = parse_string_list z in
List.iter (hide_binding state.c_proof.goal) l_s
List.iter (hide_binding state.c_proof.goal.env) l_s
));;
add_new_action
......@@ -1330,11 +1316,11 @@ add_new_action
| Scanf.Scan_failure _ ->
sscanf y "bind %s@!" (fun z ->
if z = "*" then
reveal_all_bindings state.c_proof.goal
reveal_all_bindings state.c_proof.goal.env
else
let l_string = parse_string_list z in
List.iter (reveal_binding state.c_proof.goal) l_string
List.iter (reveal_binding state.c_proof.goal.env) l_string
));;
......@@ -1902,7 +1888,7 @@ let create_guard_data_side goal encs t =
guard_enc_list = encs;
guarded_dec = Var (g_t_name,Msg) } in
let new_goal = add_t_binding goal g_t_name guarded_t in
let new_goal = add_binding goal g_t_name guarded_t in
let get_enc_content env alpha = match eiv env alpha with
| Fun ("enc",[m;r;pk]) -> m
......@@ -1920,9 +1906,9 @@ let create_guard_data_side goal encs t =
match g_u with
| Var _ -> c_goal
| _ ->
let new_c_goal = add_t_binding c_goal var_fresh g_u in
let new_c_goal = add_binding c_goal var_fresh g_u in
hide_binding new_c_goal var_fresh;
hide_binding new_c_goal.env var_fresh;
new_c_goal in
......
......@@ -102,6 +102,6 @@ let nsl_bindings =
("hr1b",h r_phi1 skb)]
let nsl = List.fold_left
(fun formula (s,t) -> Formula.add_t_binding formula s t)
(fun formula (s,t) -> Formula.add_binding formula s t)
(Formula.new_formula [] (List.combine l_phi2 r_phi2))
nsl_bindings
......@@ -2,8 +2,6 @@
(* 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.
- default_collect: if true, try to do automatic collection when adding
new bindings to the environement.
- force_color: force color using ANSI codes, in the case automatic detection
of color support of the terminal failed.
- small_size_heuristic: heuristic constant used to decide to apply the
......@@ -12,7 +10,6 @@
- input_channel: channel used to receive the proof instructions *)
type state_param =
{ shell_mode : bool;
mutable default_collect : bool;
force_color : bool;
small_size_heuristic : int;
mutable input_channel : in_channel;
......
This diff is collapsed.
......@@ -305,6 +305,57 @@ let debug_print_string_types ht =
ht);
Printf.eprintf "%!";;
exception No_such_binding of variable_string
(* hide_binding env s: Hide the binding associated with s in env. *)
let hide_binding env s =
if Hashtbl.mem env.t_bindings s then
begin
(* Sanity Check *)
assert (Hashtbl.find env.string_types s = TVar);
Hashtbl.replace env.hide_bindings s true
end
else if Hashtbl.mem env.bt_bindings s then
begin
(* Sanity Check *)
assert (Hashtbl.find env.string_types s = BTVar);
Hashtbl.replace env.hide_bindings s true
end
else
raise (No_such_binding s)
let hide_all_bindings env =
Hashtbl.filter_map_inplace
(fun s _ -> Some true)
env.hide_bindings;;
(* reveal_binding env s: Reveal the binding associated with s in env. *)
let reveal_binding env s =
if Hashtbl.mem env.t_bindings s then
begin
(* Sanity Check *)
assert (Hashtbl.find env.string_types s = TVar);
Hashtbl.replace env.hide_bindings s false
end
else if Hashtbl.mem env.bt_bindings s then
begin
(* Sanity Check *)
assert (Hashtbl.find env.string_types s = BTVar);
Hashtbl.replace env.hide_bindings s false
end
else
raise (No_such_binding s)
let reveal_all_bindings env =
Hashtbl.filter_map_inplace
(fun s _ -> Some false)
env.hide_bindings;;
(*******************)
(* Variable typing *)
......@@ -616,6 +667,52 @@ let rec get_head env term = match eiv env term with
end
| _ -> None
(* Replace a variable by a name if it is binded in the environement. This is
used after parsing a term, to disambiguate between variable and names.
Raise No_such_binding is a binding does not exist. *)
let rec set_binded_names : type a. environement -> a term -> a term =
fun env term -> match term with
| Bot -> term
| True -> term
| False -> term
| Name _ -> term
| Var (s,Msg) ->
if is_binded env s then
let s_type = Hashtbl.find env.string_types s in
if s_type = TName then
Name (s,Msg)
else
term
else
raise (No_such_binding s)
| Var (s,Bool) ->
if is_binded env s then
let s_type = Hashtbl.find env.string_types s in
if s_type = BTName then
Name (s,Bool)
else
term
else term
| Fun (s, l) ->
Fun (s, List.map (set_binded_names env) l)
| If (b, u, v) ->
If ( set_binded_names env b,
set_binded_names env u,
set_binded_names env v )
| EQ (u, v) ->
EQ ( set_binded_names env u,
set_binded_names env v )
(*****************)
(* Size Function *)
(*****************)
......@@ -700,9 +797,9 @@ let syntactic_equal : type a. environement -> a term -> a term -> bool =
(* Variable Collection *)
(***********************)
(* collect_var t s t': Collect in t all subterms t' into a term variable s.
(* collect_var_msg t s t': Collect in t all subterms t' into a term variable s.
Hack used to avoid exhaustivity warning. *)
let collect_var : type a. a term -> variable_string -> msg term -> a term =
let collect_var_msg : type a. a term -> variable_string -> msg term -> a term =
fun t s t' ->
let rec aux : type a. a term -> a term = fun t ->
......@@ -726,9 +823,9 @@ let collect_var : type a. a term -> variable_string -> msg term -> a term =
| Bool -> aux t
(* collect_bvar t s b': Collect in t all subterms b' into a booleab variable s.
(* collect_var_boole t s b': Collect in t all subterms b' into a booleab variable s.
Hack used to avoid exhaustivity warning. *)
let collect_bvar : type a. a term -> variable_string -> boole term -> a term =
let collect_var_boole : type a. a term -> variable_string -> boole term -> a term =
fun t s b' ->
let rec aux : type a. a term -> a term = fun t -> match t with
......@@ -750,6 +847,13 @@ let collect_bvar : type a. a term -> variable_string -> boole term -> a term =
| Msg -> aux t
| Bool -> b_aux t
(* collect_var t s t': Collect in t all subterms t' into a term variable s.
Hack used to avoid exhaustivity warning. *)
let collect_var : type a b. a term -> variable_string -> b term -> a term =
fun t s t' -> match get_sort t' with
| Bool -> collect_var_boole t s t'
| Msg -> collect_var_msg t s t'
(***************)
(* Collect All *)
(***************)
......@@ -817,7 +921,7 @@ let collect_all env t =
| CB (Var (s,Bool)) ->
collect_aux
(collect_bvar current_x s (Hashtbl.find env.bt_bindings s))
(collect_var current_x s (Hashtbl.find env.bt_bindings s))
(i - 1)
| _ -> failwith "collect_all: error" in
......@@ -826,6 +930,54 @@ let collect_all env t =
(*************************)
(* Add New Term Bindings *)
(*************************)
(* Raised when a binding has the wrong type. The first type is the wanted type
and the second is the already existing type. *)
exception Bad_binding of string_type * string_type
(* env_add_binding env s t: Add a new binding between the term variable s and
the term t in env. The term t must type-check. *)
let env_add_binding : type a. environement -> variable_string -> a term
-> environement =
fun env s t ->
type_check env t;
let collected_t = collect_all env t in
if Hashtbl.mem env.string_types s then
raise (Bad_binding (TVar,(Hashtbl.find env.string_types s)))
else
begin
let env' = copy_env env in
let _ = match get_sort collected_t with
| Msg -> Hashtbl.add env'.string_types s TVar
| Bool -> Hashtbl.add env'.string_types s BTVar in
Hashtbl.filter_map_inplace
(fun _ u -> Some (collect_var u s collected_t))
env'.t_bindings;
Hashtbl.filter_map_inplace
(fun _ bu -> Some (collect_var bu s collected_t))
env'.bt_bindings;
let _ = match get_sort collected_t with
| Msg -> Hashtbl.add env'.t_bindings s collected_t
| Bool -> Hashtbl.add env'.bt_bindings s collected_t in
Hashtbl.add env'.hide_bindings s true;
env'
end
(*********************)
(* Term Substitution *)
(*********************)
......@@ -1437,8 +1589,8 @@ let r_equal : type a. environement -> a term -> a term -> bool =
let nt = pseudo_normalize env t
and nt' = pseudo_normalize env t' in
let cond_nt = conds env nt
and cond_nt' = conds env nt' in
let cond_nt = List.sort_uniq (compare_cond env) (conds env nt)
and cond_nt' = List.sort_uniq (compare_cond env) (conds env nt') in
debug (fun () -> if test then
begin
......
......@@ -76,6 +76,18 @@ val string_type_to_string : string_type -> string
defined. *)
val init_env : unit -> environement
exception No_such_binding of variable_string
(* hide_binding formula s: Hide the binding associated with s in formula. *)
val hide_binding : environement -> variable_string -> unit
val hide_all_bindings : environement -> unit
(* reveal_binding formula s: Reveal the binding associated with s in formula. *)
val reveal_binding : environement -> variable_string -> unit
val reveal_all_bindings : environement -> unit
val copy_env : environement -> environement
val term_size : environement -> 'a term -> int
......@@ -144,21 +156,35 @@ val ein :
Warning: Bot is ignored and treaded as a Name *)
val get_head : environement -> msg term -> function_symbol_string option
(* Replace a variable by a name if it is binded in the environement. This is
used after parsing a term, to disambiguate between variable and names.
Raise No_such_binding is a binding does not exist. *)
val set_binded_names : environement -> 'a term -> 'a term
(***********************)
(* Variable Collection *)
(***********************)
(* collect_var t s t': Collect in t all subterms t' into a term variable s. *)
val collect_var : 'a term -> variable_string -> msg term -> 'a term
(* collect_bvar t s b': Collect in t all subterms b' into a booleab variable s. *)
val collect_bvar : 'a term -> variable_string -> boole term -> 'a term
val collect_var : 'a term -> variable_string -> 'b term -> 'a term
(* collect_all env t: Collect in t all bindings in the environement env. *)
val collect_all : environement -> 'a term -> 'a term
(*************************)
(* Add New Term Bindings *)
(*************************)
(* Raised when a binding has the wrong type. The first type is the wanted type
and the second is the already existing type. *)
exception Bad_binding of string_type * string_type
(* env_add_binding env s t: Add a new binding between the term variable s and
the term t in env. The term t must type-check. *)
val env_add_binding : environement -> variable_string -> 'a term -> environement
(************************************************)
(* Syntactic Equality modulo Variable Expantion *)
(************************************************)
......