Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

Commit 0e46a271 authored by Johannes Kanig's avatar Johannes Kanig
Browse files

close_epsilon: refactoring

parent 9ee2fb2d
......@@ -21,13 +21,6 @@ open Decl
open Task
open Term
let forall_merge vs f =
match f.f_node with
| Fquant (Fforall, fq) ->
let vs', trs, f = f_open_quant fq in
f_forall_close (vs@vs') trs f
| _ -> f_forall_close vs [] f
let is_func_ty t =
match t.Ty.ty_node with
| Ty.Tyapp (s,_) ->
......@@ -77,7 +70,7 @@ let rec rewriteT t =
(* substitute [magic] for [x] *)
let f = f_subst_single x rx f in
(* quantify over free variables and epsilon-close over [magic] *)
let f = forall_merge fv f in
let f = f_forall_close_merge fv f in
let f = t_eps_close magic_fs f in
(* apply epsilon-term to variables *)
List.fold_left (fun acc x -> t_func_app acc (t_var x)) f fv
......@@ -86,12 +79,10 @@ let rec rewriteT t =
and rewriteF f = f_map rewriteT rewriteF f
let comp t task =
match t.task_decl.td_node with
| Decl d -> add_decl task (decl_map rewriteT rewriteF d)
| _ -> add_tdecl task t.task_decl
let close d = [decl_map rewriteT rewriteF d]
let close_epsilon =
Trans.fold comp None
let close_epsilon = Trans.decl close None
let () = Trans.register_transform "close_epsilon" close_epsilon
(* TODO variable abstraction *)
......@@ -24,3 +24,14 @@
εx.P(x) => εF.(P(F@y₁@...@y_n)) where y₁...y_n are the free variable in P and
@ is the higher-order application symbol.
*)
open Term
type lambda_match =
| Flam of vsymbol list * trigger list * fmla
| Tlam of vsymbol list * trigger list * term
| LNone
val destruct_lambda : term -> lambda_match
val is_lambda : 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