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 09d9960f authored by Francois Bobot's avatar Francois Bobot
Browse files

Ajoiut des context list t dans transform

parent aa51f5fd
......@@ -9,23 +9,24 @@ let array = "Array"
let store = ["store"]
let select = ["select"]
let make_rt_rf =
let rec rt ctxt t =
let t = t_map (rt ctxt) (rf ctxt) t in
let array = find_theory ctxt.ctxt_env prelude array in
let store = (find_l array.th_export store).ls_name in
let select = (find_l array.th_export select).ls_name in
let make_rt_rf h =
let rec rt env t =
let t = t_map (rt env) (rf env) t in
let array = find_theory env prelude array in
let store = (find_ls array.th_export store).ls_name in
let select = (find_ls array.th_export select).ls_name in
match t.t_node with
| Tapp (lselect,[{t_node=Tapp(lstore,[_;a1;b])};a2])
when cloned_from ctxt lselect.ls_name select &&
cloned_from ctxt lstore.ls_name store &&
when lselect.ls_name == select &&
lstore.ls_name == store &&
t_equal_alpha a1 a2 -> b
| _ -> t
and rf ctxt f = f_map (rt ctxt) (rf ctxt) f in
rt,rf
let t () =
let rt,rf = make_rt_rf in
Transform.rewrite_map rt rf
let h = Hashtbl.create 5 in
let rt,rf = make_rt_rf h in
Transform.rewrite_env rt rf
let () = Driver.register_transform "simplify_array" t
......@@ -515,6 +515,7 @@ let find_theory env sl s =
try Mnm.find s m
with Not_found -> raise (TheoryNotFound (sl, s))
let env_tag env = env.env_tag
(** Context constructors and utilities *)
......
......@@ -153,6 +153,8 @@ exception TheoryNotFound of string list * string
val find_theory : env -> string list -> string -> theory
val env_tag : env -> int
(** Context constructors and utilities *)
type th_inst = {
......
......@@ -135,12 +135,14 @@ let transform env l =
*)
let extract_goals env drv acc th =
let ctxt = Context.use_export (Context.init_context env) th in
let ctxt = Driver.apply_before_split drv ctxt in
let l = Transform.apply Transform.split_goals ctxt in
let l = List.rev_map (fun ctxt -> (th,ctxt)) l in
List.rev_append l acc
let extract_goals =
let split_goals = Transform.split_goals () in
fun env drv acc th ->
let ctxt = Context.use_export (Context.init_context env) th in
let ctxt = Driver.apply_before_split drv ctxt in
let l = Transform.apply split_goals ctxt in
let l = List.rev_map (fun ctxt -> (th,ctxt)) l in
List.rev_append l acc
let file_sanitizer = Ident.sanitizer Ident.char_to_alnumus Ident.char_to_alnumus
......
......@@ -240,7 +240,7 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
| Rsyntaxls ((loc,q),s) ->
begin
try
let ls = (Transform.find_l th.th_export q) in
let ls = (Transform.find_ls th.th_export q) in
check_syntax loc s (List.length ls.ls_args);
add_htheory false ls.ls_name (Syntax s)
with Not_found -> errorm ~loc "Unknown logic %s"
......@@ -249,7 +249,7 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
| Rsyntaxty ((loc,q),s) ->
begin
try
let ts = Transform.find_ty th.th_export q in
let ts = Transform.find_ts th.th_export q in
check_syntax loc s (List.length ts.ts_args);
add_htheory false ts.ts_name (Syntax s)
with Not_found -> errorm ~loc "Unknown type %s"
......@@ -258,7 +258,7 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
| Rtagls (c,(loc,q),s) ->
begin
try
add_htheory c (Transform.find_l th.th_export q).ls_name
add_htheory c (Transform.find_ls th.th_export q).ls_name
(Tag (Snm.singleton s))
with Not_found -> errorm ~loc "Unknown logic %s"
(string_of_qualid qualid q)
......@@ -266,7 +266,7 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
| Rtagty (c,(loc,q),s) ->
begin
try
add_htheory c (Transform.find_ty th.th_export q).ts_name
add_htheory c (Transform.find_ts th.th_export q).ts_name
(Tag (Snm.singleton s))
with Not_found -> errorm ~loc "Unknown type %s"
(string_of_qualid qualid q)
......
......@@ -107,7 +107,7 @@ let fold isnotinlinedt isnotinlinedf ctxt0 (env, ctxt) =
| Duse _ | Dclone _ -> env,add_decl ctxt d
let t ~isnotinlinedt ~isnotinlinedf =
Transform.fold_map (fold isnotinlinedt isnotinlinedf) empty_env
Transform.fold_map (fold isnotinlinedt isnotinlinedf) (fun _ -> empty_env)
let all () = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false)
......
open Term
open Theory
let split_pos =
let rec rf acc f =
match f.f_node with
| Ftrue -> acc
| Ffalse -> f::acc
| Fapp _ -> f::acc
| Fbinop (Fand,f1,f2) -> rf (rf acc f2) f1
| Fbinop (Fimplies,f1,f2) ->
List.fold_left (fun acc f -> (f_implies f1 f)::acc)
acc (rf [] f2)
| Fbinop (Fiff,f1,f2) -> rf (rf acc (f_implies f1 f2)) (f_implies f2 f1)
| Fbinop (For,_,_) -> f::acc
| Fnot _ -> f::acc
| Fif (fif,fthen,felse) ->
rf
(rf acc (f_implies fif fthen))
(f_implies (f_not fif) felse)
| Flet (t,fb) ->
let vs,f = f_open_bound fb in
List.fold_left (fun acc f -> (f_let vs t f)::acc) acc (rf [] f)
| Fcase _ -> (* TODO better *) f::acc
| Fquant (Fforall,fmlaq) ->
let vsl,trl,fmla = f_open_quant fmlaq in
List.fold_left (fun acc f ->
(* Remove unused variable*)
(f_forall vsl trl f)::acc) acc (rf [] fmla)
| Fquant (Fexists,_) -> f::acc in
rf []
let list_fold_product f acc l1 l2 =
List.fold_left
(fun acc e1 ->
List.fold_left
(fun acc e2 -> f acc e1 e2)
l2 acc)
acc l1
let rec split_pos split_neg acc f =
let split_pos = split_pos split_neg in
match f.f_node with
| Ftrue -> acc
| Ffalse -> f::acc
| Fapp _ -> f::acc
| Fbinop (Fand,f1,f2) -> split_pos (split_pos acc f2) f1
| Fbinop (Fimplies,f1,f2) ->
list_fold_product
(fun acc f1 f2 -> (f_implies f1 f2)::acc)
acc (split_neg [] f1) (split_pos [] f2)
| Fbinop (Fiff,f1,f2) ->
split_pos (split_pos acc (f_implies f1 f2)) (f_implies f2 f1)
| Fbinop (For,f1,f2) ->
list_fold_product
(fun acc f1 f2 -> (f_or f1 f2)::acc)
acc (split_pos [] f1) (split_pos [] f2)
| Fnot _ -> List.fold_left (fun acc f -> f_not f::acc) acc (split_neg acc f)
| Fif (fif,fthen,felse) ->
split_pos
(split_pos acc (f_implies fif fthen))
(f_implies (f_not fif) felse)
| Flet (t,fb) ->
let vs,f = f_open_bound fb in
List.fold_left (fun acc f -> (f_let vs t f)::acc) acc (split_pos [] f)
| Fcase _ -> (* TODO better *) f::acc
| Fquant (Fforall,fmlaq) ->
let vsl,trl,fmla = f_open_quant fmlaq in
List.fold_left (fun acc f ->
(* TODO : Remove unused variable*)
(f_forall vsl trl f)::acc) acc (split_pos [] fmla)
| Fquant (Fexists,_) -> f::acc
let rec split_neg split_pos acc f =
let split_neg = split_neg split_pos in
match f.f_node with
| Ftrue -> f::acc
| Ffalse -> acc
| Fapp _ -> f::acc
| Fbinop (Fand,f1,f2) ->
list_fold_product
(fun acc f1 f2 -> (f_and f1 f2)::acc)
acc (split_neg [] f1) (split_neg [] f2)
| Fbinop (Fimplies,f1,f2) ->
split_pos (split_neg acc f2) f1
| Fbinop (Fiff,f1,f2) ->
(* TODO plus directe? *)
split_neg acc (f_and (f_implies f1 f2) (f_implies f2 f1))
| Fbinop (For,f1,f2) -> split_neg (split_neg acc f2) f1
| Fnot _ -> split_neg acc f
| Fif (fif,fthen,felse) ->
(split_neg acc
(f_and (f_implies fif fthen)
(f_implies (f_not fif) felse)))
| Flet (t,fb) ->
let vs,f = f_open_bound fb in
List.fold_left (fun acc f -> (f_let vs t f)::acc) acc (split_neg [] f)
| Fcase _ -> (* TODO better *) f::acc
| Fquant (Fexists,fmlaq) ->
let vsl,trl,fmla = f_open_quant fmlaq in
List.fold_left (fun acc f ->
(* TODO : Remove unused variable*)
(f_exists vsl trl f)::acc) acc (split_neg [] fmla)
| Fquant (Fforall,_) -> f::acc
let split_pos = split_pos (fun acc x -> x::acc)
let elt d =
match d.d_node with
| Dprop (Pgoal,pr,f) ->
begin
try
let l = split_pos f in
let l = split_pos [] f in
List.map (fun p -> create_prop_decl Pgoal pr p) l
with Exit -> [d]
end
......
......@@ -29,6 +29,7 @@ type 'a t = {
}
type ctxt_t = context t
type ctxt_list_t = context list t
let conv_res f c =
{ all = (fun x -> c (f.all x));
......@@ -38,6 +39,15 @@ let compose f g =
{ all = (fun x -> g.all (f.all x));
clear = (fun () -> f.clear (); g.clear ()); }
let compose' f g =
{ all = (fun x -> List.fold_left (fun acc l -> List.rev_append (g.all l) acc)
[] (f.all x));
clear = (fun () -> f.clear (); g.clear ()); }
let singleton f =
{ all = (fun x -> [f.all x]);
clear = f.clear}
let apply f x = f.all x
let clear f = f.clear ()
......@@ -66,7 +76,7 @@ let register f =
let memo_t = Hashtbl.create 17 in
t (memo f ctxt_tag memo_t) (fun () -> Hashtbl.clear memo_t)
let fold_env f_fold v_empty =
let fold f_fold v_empty =
let memo_t = Hashtbl.create 64 in
let rewind env todo =
List.fold_left
......@@ -89,25 +99,82 @@ let fold_env f_fold v_empty =
in
t (f []) (fun () -> Hashtbl.clear memo_t)
let fold f acc = fold_env f (fun _ -> acc)
let fold' (f_fold:context -> 'a -> 'a list) v_empty =
let memo_t = Hashtbl.create 64 in
let rewind env todo =
List.fold_left
(fun env ctxt ->
let env = List.fold_left
(fun acc e -> List.rev_append (f_fold ctxt e) acc) [] env in
Hashtbl.add memo_t ctxt.ctxt_tag env;
env)
env todo
in
let rec f todo ctxt =
match ctxt.ctxt_prev with
| None ->
rewind [v_empty ctxt.ctxt_env] todo
| Some ctxt2 ->
try
let env = Hashtbl.find memo_t ctxt2.ctxt_tag in
rewind env (ctxt :: todo)
with Not_found ->
f (ctxt :: todo) ctxt2
in
t (f []) (fun () -> Hashtbl.clear memo_t)
let fold_map f_fold v_empty =
let v_empty env = v_empty, init_context env in
conv_res (fold_env f_fold v_empty) snd
let v_empty env = v_empty env, init_context env in
conv_res (fold f_fold v_empty) snd
let fold_map' f_fold v_empty =
let v_empty env = v_empty env, init_context env in
conv_res (fold' f_fold v_empty) (List.map snd)
let map f_map =
fold_map (fun ctxt1 ctxt2 -> (), f_map ctxt1 (snd ctxt2)) ()
fold (fun ctxt1 ctxt2 -> f_map ctxt1 ctxt2) init_context
let map' f_map =
fold' (fun ctxt1 ctxt2 -> f_map ctxt1 ctxt2) init_context
let map_concat f_elt =
let f_elt ctxt0 ctxt = List.fold_left add_decl ctxt (f_elt ctxt0) in
map f_elt
let map_concat' f_elt =
let f_elt ctxt0 ctxt = List.map (List.fold_left add_decl ctxt) (f_elt ctxt0) in
map' f_elt
let elt f_elt =
let memo_elt = Hashtbl.create 64 in
let f_elt ctxt0 = memo f_elt d_tag memo_elt ctxt0.ctxt_decl in
let f = map_concat f_elt in
{ f with clear = fun () -> Hashtbl.clear memo_elt; f.clear () }
let elt' f_elt =
let memo_elt = Hashtbl.create 64 in
let f_elt ctxt0 = memo f_elt d_tag memo_elt ctxt0.ctxt_decl in
let f = map_concat' f_elt in
{ f with clear = fun () -> Hashtbl.clear memo_elt; f.clear () }
let elt_env f_elt =
let f_elt env =
let memo_elt = Hashtbl.create 64 in
memo (f_elt env) d_tag memo_elt in
let memo_env = Hashtbl.create 2 in
let f_elt ctxt = (memo f_elt env_tag memo_env ctxt.ctxt_env) ctxt.ctxt_decl in
let f = map_concat f_elt in
{ f with clear = fun () -> Hashtbl.clear memo_env; f.clear () }
let elt_env' f_elt =
let f_elt env =
let memo_elt = Hashtbl.create 64 in
memo (f_elt env) d_tag memo_elt in
let memo_env = Hashtbl.create 2 in
let f_elt ctxt = (memo f_elt env_tag memo_env ctxt.ctxt_env) ctxt.ctxt_decl in
let f = map_concat' f_elt in
{ f with clear = fun () -> Hashtbl.clear memo_env; f.clear () }
(* Utils *)
......@@ -131,7 +198,7 @@ let fold_context_of_decl f ctxt env ctxt_done d =
let env,decls = f ctxt env d in
env,List.fold_left add_decl ctxt_done decls
let split_goals =
let split_goals () =
let f ctxt0 (ctxt,l) =
let decl = ctxt0.ctxt_decl in
match decl.d_node with
......@@ -143,7 +210,7 @@ let split_goals =
add_decl ctxt d2 :: l)
| _ -> (add_decl ctxt decl, l)
in
let g = fold_env f (fun env -> init_context env, []) in
let g = fold f (fun env -> init_context env, []) in
conv_res g snd
let remove_lemma =
......@@ -184,17 +251,25 @@ let rewrite_elt rt rf d =
|Dprop (k,pr,f) -> [create_prop_decl k pr (rf f)]
|Duse _ |Dclone _ -> [d]
let rewrite_env rt rf env =
let rt = rt env in
let rf = rf env in
rewrite_elt rt rf
let rewrite_elt rt rf = elt (rewrite_elt rt rf)
let rec find_l ns = function
let rewrite_env rt rf =
elt_env (rewrite_env rt rf)
let rec find_ls ns = function
| [] -> assert false
| [a] -> Mnm.find a ns.ns_ls
| a::l -> find_l (Mnm.find a ns.ns_ns) l
| a::l -> find_ls (Mnm.find a ns.ns_ns) l
let rec find_ty ns = function
let rec find_ts ns = function
| [] -> assert false
| [a] -> Mnm.find a ns.ns_ts
| a::l -> find_ty (Mnm.find a ns.ns_ns) l
| a::l -> find_ts (Mnm.find a ns.ns_ns) l
let rec find_pr ns = function
| [] -> assert false
......
......@@ -27,11 +27,17 @@ open Theory
(* The type of transformation from list of 'a to list of 'b *)
type 'a t
type ctxt_t = context t
type ctxt_list_t = context list t
(* compose two transformations, the underlying datastructures for
the memoisation are shared *)
val compose : context t -> 'a t -> 'a t
val compose' : context list t -> 'a list t -> 'a list t
val singleton : 'a t -> 'a list t
(* apply a transformation and memoise *)
val apply : 'a t -> context -> 'a
......@@ -41,29 +47,47 @@ val register : (context -> 'a) -> 'a t
(* Fold from the first declaration to the last with a memoisation at
each step *)
val fold : (context -> 'a -> 'a) -> 'a -> 'a t
(* val fold : (context -> 'a -> 'a) -> 'a -> 'a t *)
val fold : (context -> 'a -> 'a) -> (env -> 'a) -> 'a t
val fold' : (context -> 'a -> 'a list) -> (env -> 'a) -> 'a list t
val fold_env : (context -> 'a -> 'a) -> (env -> 'a) -> 'a t
val fold_map : (context -> 'a * context -> 'a * context)
-> (env -> 'a) -> context t
(* via fold *)
val fold_map : (context -> 'a * context -> 'a * context) -> 'a -> context t
val fold_map' : (context -> 'a * context -> ('a * context) list)
-> (env -> 'a) -> context list t
val map : (context -> context -> context) -> context t
(* via fold *)
val map' : (context -> context -> context list) -> context list t
(*
val map_concat : (context -> decl list) -> context t
val map_concat' : (context -> decl list list) -> context list t
*)
(* map the element of the list without an environnment.
A memoisation is performed at each step, and for each elements *)
val elt : (decl -> decl list) -> context t
(* via map *)
val elt' : (decl -> decl list list) -> context list t
val elt_env : (env -> (decl -> decl list)) -> context t
(* via map *)
val elt_env' : (env -> (decl -> decl list list)) -> context list t
(** Utils *)
(* Utils *)
val split_goals : context list t
val remove_lemma : context t
val split_goals : unit -> context list t
exception NotGoalContext
val goal_of_ctxt : context -> prop
......@@ -76,10 +100,21 @@ val identity : context t
val rewrite_elt :
(Term.term -> Term.term) ->
(Term.fmla -> Term.fmla) -> context t
(* via elt *)
val rewrite_env :
(env -> Term.term -> Term.term) ->
(env -> Term.fmla -> Term.fmla) -> context t
(* via elt_env *)
(*val rewrite_map :
(context -> Term.term -> Term.term) ->
(context -> Term.fmla -> Term.fmla) -> context t
(* via map *)
*)
val cloned_from : context -> ident -> ident -> bool
val find_ty : namespace -> string list -> Ty.tysymbol
val find_l : namespace -> string list -> Term.lsymbol
val find_ts : namespace -> string list -> Ty.tysymbol
val find_ls : namespace -> string list -> Term.lsymbol
val find_pr : namespace -> string list -> prop
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