Commit f6eed821 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

environment type is now abstract

parent 5aad657b
Pipeline #1645 passed with stage
in 2 minutes and 44 seconds
......@@ -237,13 +237,6 @@ let reveal_element formula i =
(* Binders Handling *)
(********************)
let size_t_bindings formula = Hashtbl.length formula.env.t_bindings
let size_bt_bindings formula = Hashtbl.length formula.env.bt_bindings
let size_bindings formula =
(size_t_bindings formula) + (size_bt_bindings 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. *)
let add_binding : type a. formula -> variable_string -> a term -> formula =
......@@ -267,78 +260,22 @@ let add_binding : type a. formula -> variable_string -> a term -> formula =
(* remove_binding formula s: Remove the binding associated with s in formula. *)
let remove_binding formula s =
if Hashtbl.mem formula.env.t_bindings s then
begin
(* Sanity Check *)
assert (Hashtbl.find formula.env.string_types s = TVar);
let env' = copy_env formula.env in
Hashtbl.filter_map_inplace
(fun _ u -> Some (expand_var formula.env u s))
env'.t_bindings;
Hashtbl.filter_map_inplace
(fun _ bu -> Some (expand_var formula.env bu s))
env'.bt_bindings;
let f' = List.map (fun entry ->
match entry.term_pair with
| T (u,v) ->
update_term_pair entry (T (expand_var formula.env u s,
expand_var formula.env v s))
| B (bu,bv) ->
update_term_pair entry (B (expand_var formula.env bu s,
expand_var formula.env bv s)))
formula.formula_element_list in
Hashtbl.remove env'.string_types s;
Hashtbl.remove env'.t_bindings s;
Hashtbl.remove env'.hide_bindings s;
{ formula_element_list = f';
env = env' }
end
else if Hashtbl.mem formula.env.bt_bindings s then
begin
(* Sanity Check *)
assert (Hashtbl.find formula.env.string_types s = BTVar);
let env' = copy_env formula.env in
Hashtbl.filter_map_inplace
(fun _ u -> Some (expand_var formula.env u s))
env'.t_bindings;
Hashtbl.filter_map_inplace
(fun _ bu -> Some (expand_var formula.env bu s))
env'.bt_bindings;
let f' = List.map (fun entry ->
match entry.term_pair with
| T (u,v) ->
update_term_pair entry (T (expand_var formula.env u s,
expand_var formula.env v s))
let f' = List.map (fun entry ->
match entry.term_pair with
| T (u,v) ->
update_term_pair entry (T (expand_var formula.env u s,
expand_var formula.env v s))
| B (bu,bv) ->
update_term_pair entry (B (expand_var formula.env bu s,
expand_var formula.env bv s)))
| B (bu,bv) ->
update_term_pair entry (B (expand_var formula.env bu s,
expand_var formula.env bv s)))
formula.formula_element_list in
formula.formula_element_list in
Hashtbl.remove env'.string_types s;
Hashtbl.remove env'.bt_bindings s;
Hashtbl.remove env'.hide_bindings s;
let env' = env_remove_binding formula.env s in
{ formula_element_list = f';
env = env' }
end
else
raise (No_such_binding s)
{ formula_element_list = f';
env = env' }
(* clean_bindings formula : Remove all bindings that are unused. *)
......@@ -356,9 +293,9 @@ let clean_bindings formula =
|| (subterm formula.env (Var (var,sort)) u'))
formula.formula_element_list in
let f_fold : type a. variable_string -> a term -> variable_string list ->
let f_fold : type a. variable_string list -> (variable_string * a term) ->
variable_string list =
fun var t acc ->
fun acc (var, t) ->
if appears (get_sort t) var then
acc
else
......@@ -366,10 +303,10 @@ let clean_bindings formula =
let to_remove = match sort with
| Msg ->
Hashtbl.fold f_fold formula.env.t_bindings []
List.fold_left f_fold [] (get_bindings formula.env Msg)
| Bool ->
Hashtbl.fold f_fold formula.env.bt_bindings [] in
List.fold_left f_fold [] (get_bindings formula.env Bool) in
List.fold_left remove_binding formula to_remove in
......@@ -454,44 +391,6 @@ let rec print_lor_formula shell_mode lor_bool cpt f =
let hashtbl_to_list ht =
List.rev (Hashtbl.fold (fun a b acc -> (a,b) :: acc) ht [])
(* Print the formula let bindings of sort term. *)
let print_t_bindings formula shell_mode =
let open Fmt in
let ident ppf s = pf ppf "%s" s in
list ~sep:nop
(fun ppf (s,t) ->
if not (Hashtbl.find formula.env.hide_bindings s) then
pf ppf "%a@[%a@]@."
(styled `Bold (styled `Magenta ident)) (Printf.sprintf "%s:" s)
print_term t)
stdout
(List.stable_sort
(fun (k,_) (k',_) -> Pervasives.compare k k')
(Hashtbl.fold (fun k v acc -> (k,v) :: acc) formula.env.t_bindings []))
(* Print the formula let bindings of sort bool *)
let print_bt_bindings formula shell_mode =
let open Fmt in
let ident ppf s = pf ppf "%s" s in
list ~sep:nop
(fun ppf (s,b) ->
if not (Hashtbl.find formula.env.hide_bindings s) then
pf ppf "%a@[%a@]"
(styled `Bold (styled `Magenta ident)) (Printf.sprintf "%s:" s)
print_term b)
stdout
(List.stable_sort
(fun (k,_) (k',_) -> Pervasives.compare k k')
(Hashtbl.fold (fun k v acc -> (k,v) :: acc) formula.env.bt_bindings []))
(* Colored pretty printing of the formula on stdout. *)
let print_formula formula param =
let shell_mode = param.shell_mode in
......@@ -516,16 +415,14 @@ let print_formula formula param =
print_lor_formula shell_mode false 0 formula.formula_element_list;
(* Print the bindings *)
let bindings_to_print =
Hashtbl.fold (fun _ b b' -> (not b) || b')
formula.env.hide_bindings false in
let print_bindings = bindings_to_print formula.env in
if bindings_to_print then
if print_bindings then
begin
print_separator shell_mode;
next_line shell_mode;
print_t_bindings formula shell_mode;
print_bt_bindings formula shell_mode;
print_t_bindings formula.env shell_mode;
print_bt_bindings formula.env shell_mode;
end;;
......@@ -563,37 +460,6 @@ let rec print_lor_formula_latex channel lor_bool cpt f =
print_lor_formula_latex channel lor_bool (cpt + 1) tail
(* Print latex code for the formula let bindings of sort term. *)
let print_t_bindings_latex channel env =
Hashtbl.iter
(fun s t ->
Printf.fprintf channel "%s &" s;
print_term_latex channel t;
Printf.fprintf channel "\\\\\\hline\n")
env.t_bindings
(* Print latex code for the formula let bindings of sort bool. *)
let print_bt_bindings_latex channel env =
Hashtbl.iter
(fun s bt ->
Printf.fprintf channel "%s &" s;
print_term_latex channel bt;
Printf.fprintf channel "\\\\\\hline\n")
env.bt_bindings
(* Print latex code for all the bindings. *)
let print_bindings_latex channel env =
Printf.fprintf channel "\\begin{array}{|l|l|}\n\\hline\n";
print_t_bindings_latex channel env;
Printf.fprintf channel "\\end{array}\n";
Printf.fprintf channel "\\begin{array}{|l|l|}\n\\hline\n";
print_bt_bindings_latex channel env;
Printf.fprintf channel "\\end{array}\n";;
let print_formula_latex channel formula =
(* Print the left formula *)
Printf.fprintf channel "\\begin{array}{c}\n";
......
......@@ -344,7 +344,7 @@ let rec fresh_name env map_fresh side s =
(sside, map_fresh') in
(* If fresh_s was already used then reiterate the process. *)
if Hashtbl.mem env.string_types fresh_s then
if is_binded env fresh_s then
fresh_name env map_fresh' side s
else
begin
......
......@@ -197,47 +197,6 @@ let print_term_stderr t =
print_term Fmt.stderr t;
Fmt.pf Fmt.stderr "@?";;
(******************************)
(* Latex Term Pretty Printing *)
(******************************)
(* Auxilliary function used to build term printing functions. *)
let rec print_term_latex : type a. out_channel -> a term -> unit =
fun channel t ->
match t with
| Bot -> fprintf channel "\tbot{}";
| Name (s,Msg) -> fprintf channel "\\nonce{%s}" s
| Name (s,Bool) -> fprintf channel "\\bnonce{%s}" s
| True -> fprintf channel "\\true{}"
| False -> fprintf channel "\\false{}"
| Var (s,Msg) -> fprintf channel "\\lbind{%s}" s
| Var (s,Bool) -> fprintf channel "\\blbind{%s}" s
| EQ (u,v) ->
fprintf channel "\\eq{%a}{%a}"
print_term_latex u
print_term_latex v;
| Fun ("pair",l) ->
begin match l with
| a :: [b] ->
fprintf channel "\\pair{%a}{%a}"
print_term_latex a
print_term_latex b;
| _ -> failwith "latex term printing: pair: wrong number of elements"
end
| Fun (s,l) ->
begin match l with
|[] -> fprintf channel "\\fname{%s}()" s
| h :: tail ->
fprintf channel "\\fname{%s}(%a%a)" s
print_term_latex h
(fun channel l -> List.iter (fun t ->
fprintf channel ", %a" print_term_latex t) l) tail;
end
| If (b,u,v) ->
fprintf channel "\\ite{%a}{%a}{%a}"
print_term_latex b
print_term_latex u
print_term_latex v;;
(****************)
......@@ -262,6 +221,53 @@ type environment =
hide_bindings : (variable_string, bool) Hashtbl.t;
string_types : (string, string_type) Hashtbl.t }
(*******************************)
(* Environment Pretty Printing *)
(*******************************)
(* Print the formula let bindings of sort term. *)
let print_t_bindings env shell_mode =
let open Fmt in
let ident ppf s = pf ppf "%s" s in
list ~sep:nop
(fun ppf (s,t) ->
if not (Hashtbl.find env.hide_bindings s) then
pf ppf "%a@[%a@]@."
(styled `Bold (styled `Magenta ident)) (Printf.sprintf "%s:" s)
print_term t)
stdout
(List.stable_sort
(fun (k,_) (k',_) -> Pervasives.compare k k')
(Hashtbl.fold (fun k v acc -> (k,v) :: acc) env.t_bindings []))
(* Print the formula let bindings of sort bool *)
let print_bt_bindings env shell_mode =
let open Fmt in
let ident ppf s = pf ppf "%s" s in
list ~sep:nop
(fun ppf (s,b) ->
if not (Hashtbl.find env.hide_bindings s) then
pf ppf "%a@[%a@]"
(styled `Bold (styled `Magenta ident)) (Printf.sprintf "%s:" s)
print_term b)
stdout
(List.stable_sort
(fun (k,_) (k',_) -> Pervasives.compare k k')
(Hashtbl.fold (fun k v acc -> (k,v) :: acc) env.bt_bindings []))
let bindings_to_print env =
Hashtbl.fold (fun _ b b' -> (not b) || b')
env.hide_bindings false
(*****************)
(* Miscellaneous *)
(*****************)
......@@ -297,6 +303,13 @@ let copy_env env =
hide_bindings = Hashtbl.copy env.hide_bindings;
string_types = Hashtbl.copy env.string_types }
let size_t_bindings env = Hashtbl.length env.t_bindings
let size_bt_bindings env = Hashtbl.length env.bt_bindings
let size_bindings formula =
(size_t_bindings formula) + (size_bt_bindings formula)
let get_bindings : type a. environment -> a sort
-> (variable_string * a term) list =
fun env sort -> match sort with
......@@ -1009,6 +1022,42 @@ let env_add_binding : type a. environment -> variable_string -> a term
env''
end
(* env_remove_binding env s: Remove the binding associated with s in env. *)
let env_remove_binding env s =
let is_tvar = Hashtbl.mem env.t_bindings s
and is_btvar = Hashtbl.mem env.bt_bindings s in
if (not is_tvar) && (not is_btvar ) then
raise (No_such_binding s);
if is_tvar then
assert (Hashtbl.find env.string_types s = TVar);
if is_btvar then
assert (Hashtbl.find env.string_types s = BTVar);
let env' = copy_env env in
Hashtbl.filter_map_inplace
(fun _ u -> Some (expand_var env u s))
env'.t_bindings;
Hashtbl.filter_map_inplace
(fun _ bu -> Some (expand_var env bu s))
env'.bt_bindings;
Hashtbl.remove env'.string_types s;
Hashtbl.remove env'.hide_bindings s;
if is_tvar then
Hashtbl.remove env'.t_bindings s;
if is_btvar then
Hashtbl.remove env'.bt_bindings s;
env'
(*********************)
(* Term Substitution *)
......@@ -1017,8 +1066,7 @@ let env_add_binding : type a. environment -> variable_string -> a term
(* var_subst s u t: Replace Var s by u in t: t[u/s].
Be careful, this does not apply the substitution in the environment!
No type-checking is done. *)
let rec var_subst :
type a. variable_string -> msg term -> a term -> a term =
let rec var_subst : type a. variable_string -> msg term -> a term -> a term =
fun s u t -> match t with
| Bot -> t
| True -> t
......@@ -1655,3 +1703,78 @@ let r_equal : type a. environment -> a term -> a term -> bool =
|| ((eq_aux u v') && (eq_aux v u'))
| Var _,_ | _,Var _ -> assert false
| _ -> syntactic_equal env nt nt'
(******************)
(* Latex Printing *)
(******************)
(* Auxilliary function used to build term printing functions. *)
let rec print_term_latex : type a. out_channel -> a term -> unit =
fun channel t ->
match t with
| Bot -> fprintf channel "\tbot{}";
| Name (s,Msg) -> fprintf channel "\\nonce{%s}" s
| Name (s,Bool) -> fprintf channel "\\bnonce{%s}" s
| True -> fprintf channel "\\true{}"
| False -> fprintf channel "\\false{}"
| Var (s,Msg) -> fprintf channel "\\lbind{%s}" s
| Var (s,Bool) -> fprintf channel "\\blbind{%s}" s
| EQ (u,v) ->
fprintf channel "\\eq{%a}{%a}"
print_term_latex u
print_term_latex v;
| Fun ("pair",l) ->
begin match l with
| a :: [b] ->
fprintf channel "\\pair{%a}{%a}"
print_term_latex a
print_term_latex b;
| _ -> failwith "latex term printing: pair: wrong number of elements"
end
| Fun (s,l) ->
begin match l with
|[] -> fprintf channel "\\fname{%s}()" s
| h :: tail ->
fprintf channel "\\fname{%s}(%a%a)" s
print_term_latex h
(fun channel l -> List.iter (fun t ->
fprintf channel ", %a" print_term_latex t) l) tail;
end
| If (b,u,v) ->
fprintf channel "\\ite{%a}{%a}{%a}"
print_term_latex b
print_term_latex u
print_term_latex v;;
(* Print latex code for the formula let bindings of sort term. *)
let print_t_bindings_latex channel env =
Hashtbl.iter
(fun s t ->
Printf.fprintf channel "%s &" s;
print_term_latex channel t;
Printf.fprintf channel "\\\\\\hline\n")
env.t_bindings
(* Print latex code for the formula let bindings of sort bool. *)
let print_bt_bindings_latex channel env =
Hashtbl.iter
(fun s bt ->
Printf.fprintf channel "%s &" s;
print_term_latex channel bt;
Printf.fprintf channel "\\\\\\hline\n")
env.bt_bindings
(* Print latex code for all the bindings. *)
let print_bindings_latex channel env =
Printf.fprintf channel "\\begin{array}{|l|l|}\n\\hline\n";
print_t_bindings_latex channel env;
Printf.fprintf channel "\\end{array}\n";
Printf.fprintf channel "\\begin{array}{|l|l|}\n\\hline\n";
print_bt_bindings_latex channel env;
Printf.fprintf channel "\\end{array}\n";;
......@@ -59,14 +59,23 @@ type string_type =
| TName (* Name of sort term *)
| BTName (* Name of sort bool *)
type environment =
{ t_bindings : (variable_string, msg term) Hashtbl.t;
bt_bindings : (variable_string, boole term) Hashtbl.t;
hide_bindings : (variable_string, bool) Hashtbl.t;
string_types : (string, string_type) Hashtbl.t }
type environment (* = *)
(* { t_bindings : (variable_string, msg term) Hashtbl.t; *)
(* bt_bindings : (variable_string, boole term) Hashtbl.t; *)
(* hide_bindings : (variable_string, bool) Hashtbl.t; *)
(* string_types : (string, string_type) Hashtbl.t } *)
exception Not_type_checking of string
(*******************************)
(* Environment Pretty Printing *)
(*******************************)
val print_t_bindings : environment -> bool -> unit
val print_bt_bindings : environment -> bool -> unit
val bindings_to_print : environment -> bool
(*****************)
(* Miscellaneous *)
......@@ -80,7 +89,6 @@ val init_env : unit -> environment
val get_bindings : environment -> 'a sort -> (variable_string * 'a term) list
exception No_such_binding of variable_string
(* hide_binding formula s: Hide the binding associated with s in formula. *)
......@@ -190,6 +198,8 @@ exception Bad_binding of string_type * string_type
the term t in env. The term t must type-check. *)
val env_add_binding : environment -> variable_string -> 'a term -> environment
(* env_remove_binding env s: Remove the binding associated with s in env. *)
val env_remove_binding : environment -> variable_string -> environment
(************************************************)
(* Syntactic Equality modulo Variable Expantion *)
......
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