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

functional implementation of maps. Now this is slower ...

parent f6eed821
Pipeline #1647 passed with stage
in 2 minutes and 25 seconds
......@@ -105,14 +105,12 @@ let cut l i =
(* bind formula my_fun: Return a new formula where my_fun has been applied to
the formula elements. Check that the new formula is type checking. *)
let bind formula my_fun =
let env' = copy_env formula.env in
let f' = my_fun formula.formula_element_list in
let env'' = type_check_formula_element_list env' f' in
let env' = type_check_formula_element_list formula.env f' in
{ formula_element_list = f';
env = env'' }
env = env' }
(* c_bind formula new_f: Return a new formula where the formula elements
have been replaced by new_f. *)
......
......@@ -1504,11 +1504,11 @@ let auto_ift state =
(0,[])
goal.formula_element_list in
debug (fun () -> List.iter (fun (r,i) ->
Fmt.pf Fmt.stderr "%d " i;
print_rule_long Fmt.stderr r;
Fmt.pf Fmt.stderr "\n@?";)
ift_rule_list);
(* debug (fun () -> List.iter (fun (r,i) -> *)
(* Fmt.pf Fmt.stderr "%d " i; *)
(* print_rule_long Fmt.stderr r; *)
(* Fmt.pf Fmt.stderr "\n@?";) *)
(* ift_rule_list); *)
unary_aux state (List.rev ift_rule_list)
......
......@@ -347,9 +347,7 @@ let rec fresh_name env map_fresh side s =
if is_binded env fresh_s then
fresh_name env map_fresh' side s
else
begin
(fresh_s, map_fresh')
end
(* Guard are conjunctions of positive and negative boolean terms.
Intuitively, Conj (b, g) ~ Conj (Guard b, g)
......@@ -1045,11 +1043,7 @@ let fold f_conf =
List.fold_left
(fun acc action ->
(* Environement are updated in place, so we need to make a copy for
each action. *)
let f_conf' = { f_conf with f_env = copy_env f_conf.f_env } in
( apply_action action Left f_conf'
( apply_action action Left f_conf
|> apply_action action Right )
:: acc )
[]
......
This diff is collapsed.
......@@ -26,7 +26,6 @@ type _ term =
val get_sort : 'a term -> 'a sort
(* term_free_variables t : Return the lists (free,b_free) of, respectively,
free Msg variables and free Bool variables in the term t. *)
val term_free_variables : 'a term -> variable_string list * variable_string list
......@@ -55,17 +54,12 @@ type string_type =
| TVar (* Term variable *)
| BTVar (* Boolean term variable *)
| TFun of int (* Function symbol of sort term with arity *)
| BTFun of int (* Function symbol of sort bool with arity *)
| TName (* Name of sort term *)
| BTName (* Name of sort bool *)
| BTFun of int (* Function symbol of sort bool with arity *)
| 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
exception Not_type_checking of string
(*******************************)
(* Environment Pretty Printing *)
......@@ -77,14 +71,14 @@ val print_bt_bindings : environment -> bool -> unit
val bindings_to_print : environment -> bool
(*****************)
(* Miscellaneous *)
(*****************)
val string_type_to_string : string_type -> string
(* Return an initial environment, with the basic function symbols' sort
defined. *)
(* Return an initial environment, with the basic function symbol defined. *)
val init_env : unit -> environment
val get_bindings : environment -> 'a sort -> (variable_string * 'a term) list
......@@ -101,17 +95,13 @@ val reveal_binding : environment -> variable_string -> environment
val reveal_all_bindings : environment -> environment
val copy_env : environment -> environment
val term_size : environment -> 'a term -> int
(*******************)
(* Variable typing *)
(*******************)
(* Variable typing:
- the environment is modified in-place if type-checking succeed.
- if the type-checking fails, no modifications are done. *)
exception Not_type_checking of string
(* Return true iff s is binded in the environment. *)
val is_binded : environment -> string -> bool
......@@ -128,9 +118,8 @@ val bind_type : environment -> string -> string_type -> environment
already binded in env, raise a Not_type_checking exception. *)
val bind_new_type : environment -> string -> string_type -> environment
(* type_check env t: Type-checks the term t in env. Update the environment env
if the type checking is successful. *)
val type_check : environment -> 'a term -> environment
(* type_check t env: Type-checks the term t in env. *)
val type_check : 'a term -> environment -> environment
(* type_check_all env l_term b_term: Type-checks all elements in l_term and
b_term in the environment env. *)
......@@ -201,15 +190,6 @@ 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 *)
(************************************************)
(* Syntactic equality modulo the environment. *)
val syntactic_equal : environment -> 'a term -> 'a term -> bool
(* R-equality modulo the environment. *)
val r_equal : environment -> 'a term -> 'a term -> bool
(*********************)
(* Term Substitution *)
......@@ -244,6 +224,7 @@ val all_subterms : environment -> 'a term -> 'b sort -> ('b term -> bool)
val const_subterm : environment -> msg term -> msg term -> msg term list
-> bool
(**********************)
(* Term Normalization *)
(**********************)
......@@ -261,3 +242,14 @@ val weak_normalize : environment -> 'a term -> 'a term
(* pseudo_normalize env t : Return a pseudo-normalisation of t (i.e. a R-normal
for a arbitrary total ordering on R-normal if-free conditionals.). *)
val pseudo_normalize : environment -> 'a term -> 'a term
(************************************************)
(* Syntactic Equality modulo Variable Expantion *)
(************************************************)
(* Syntactic equality modulo the environment. *)
val syntactic_equal : environment -> 'a term -> 'a term -> bool
(* R-equality modulo the environment. *)
val r_equal : environment -> 'a term -> 'a term -> bool
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