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 4312fe07 authored by Johannes Kanig's avatar Johannes Kanig
Browse files

close epsilon transformation

parent 9fdfcea6
......@@ -130,7 +130,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
libencoding encoding_decorate encoding_bridge \
encoding_explicit encoding_simple2 \
encoding_instantiate simplify_array filter_trigger \
introduction abstraction
introduction abstraction close_epsilon
LIB_PRINTER = print_real alt_ergo why3 smt coq tptp simplify gappa
......
......@@ -8,3 +8,4 @@ theory BuiltIn
syntax type real "real"
syntax logic (=) "(%1 = %2)"
end
......@@ -17,6 +17,9 @@ theory Map
use export int.Int
logic double (l : list int) : list int = map (\ i : int . i * 2) l
logic double_let (l : list int) : list int =
let x = 2 in
map (\ i : int . i * x) l
logic lequal (l1 l2 : list int) = forall2 (\ i1 i2 : int . i1 = i2) l1 l2
end
......@@ -38,6 +41,7 @@ theory Test1
use export int.Int
use export list.List
use export list.Length
use Map as M
goal G1 : length (Cons 1 Nil) = 1
goal G2 : length (Cons 1 (Cons 2 Nil)) = 1 + 1
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Theory
open Decl
open Task
open Term
let rec rewriteT t = match t.t_node with
| Teps fb ->
let fv = Svs.elements (t_freevars Svs.empty t) in
let x, f = f_open_bound fb in
let f = rewriteF f in
if fv = [] then t_eps_close x f
else
(* the type, symbol and term of the new epsilon-symbol [magic] *)
let magic_ty =
List.fold_right (fun x acc -> Ty.ty_func x.vs_ty acc) fv x.vs_ty in
let magic_fs = create_vsymbol (Ident.id_fresh "f") magic_ty in
let magic_f = t_var magic_fs in
(* the application of [magic] to the free variables *)
let rx =
List.fold_left (fun acc x -> t_func_app acc (t_var x)) magic_f fv in
(* substitute [magic] for [x] *)
let f = f_subst_single x rx f in
(* quantify over free variables and epsilon-close over [magic] *)
let f = f_forall_close_simp 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
| _ ->
t_map rewriteT rewriteF 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_epsilon =
Trans.fold comp None
let () = Trans.register_transform "close_epsilon" close_epsilon
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(** The aim of this translation is to obtain terms where all epsilon
* abstractions are closed *)
(** We do this by applying the following rewriting rule:
ε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.
*)
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