Commit acbaa9b7 authored by François Bobot's avatar François Bobot
Browse files

guard : merge quantifiers without triggers

parent 02876411
...@@ -113,6 +113,18 @@ module Transform = struct ...@@ -113,6 +113,18 @@ module Transform = struct
Term.create_lsymbol (id_clone lsymbol.ls_name) args lsymbol.ls_value) Term.create_lsymbol (id_clone lsymbol.ls_name) args lsymbol.ls_value)
(** {1 transformations} *) (** {1 transformations} *)
(** todo use callback for this one *)
let rec f_open_all_quant q f = match f.f_node with
| Fquant (q', f) when q' = q ->
let vl, tr, f = f_open_quant f in
begin match tr with
| [] ->
let vl', tr, f = f_open_all_quant q f in
vl@vl', tr, f
| _ -> vl, tr, f
end
| _ -> [], [], f
(** translation of terms *) (** translation of terms *)
let rec term_transform kept varM t = let rec term_transform kept varM t =
...@@ -130,14 +142,14 @@ module Transform = struct ...@@ -130,14 +142,14 @@ module Transform = struct
| Fapp(p,terms) -> | Fapp(p,terms) ->
let terms = List.map (term_transform kept varM) terms in let terms = List.map (term_transform kept varM) terms in
f_app (findL p) terms f_app (findL p) terms
| Fquant(q,b) -> | Fquant(q,_) ->
let vsl,trl,fmla,cb = f_open_quant_cb b in let vsl,trl,fmla = f_open_all_quant q f in
let fmla = fmla_transform kept varM fmla in let fmla = fmla_transform kept varM fmla in
let fmla2 = guard q kept varM fmla vsl in let fmla2 = guard q kept varM fmla vsl in
(* TODO : how to modify the triggers? *) (* TODO : how to modify the triggers? *)
let trl = tr_map (term_transform kept varM) let trl = tr_map (term_transform kept varM)
(fmla_transform kept varM) trl in (fmla_transform kept varM) trl in
f_quant q (cb vsl trl fmla2) f_quant q (f_close_quant vsl trl fmla2)
| _ -> (* otherwise : just traverse and translate *) | _ -> (* otherwise : just traverse and translate *)
f_map (term_transform kept varM) (fmla_transform kept varM) f(* in *) f_map (term_transform kept varM) (fmla_transform kept varM) f(* in *)
(* Format.eprintf "fmla_to : %a@." Pretty.print_fmla f;f *) (* Format.eprintf "fmla_to : %a@." Pretty.print_fmla f;f *)
...@@ -165,8 +177,8 @@ module Transform = struct ...@@ -165,8 +177,8 @@ module Transform = struct
and f_type_close_select kept f' = and f_type_close_select kept f' =
let tvs = f_ty_freevars Stv.empty f' in let tvs = f_ty_freevars Stv.empty f' in
let rec trans fn acc f = match f.f_node with let rec trans fn acc f = match f.f_node with
| Fquant(Fforall as q,b) -> (* Exists same thing? *) | Fquant(Fforall as q,_) -> (* Exists same thing? *)
let vsl,trl,fmla,cb = f_open_quant_cb b in let vsl,trl,fmla = f_open_all_quant q f in
let add acc vs = (t_var vs)::acc in let add acc vs = (t_var vs)::acc in
let acc = List.fold_left add acc vsl in let acc = List.fold_left add acc vsl in
let fn varM f = let fn varM f =
...@@ -174,7 +186,7 @@ module Transform = struct ...@@ -174,7 +186,7 @@ module Transform = struct
(* TODO : how to modify the triggers? *) (* TODO : how to modify the triggers? *)
let trl = tr_map (term_transform kept varM) let trl = tr_map (term_transform kept varM)
(fmla_transform kept varM) trl in (fmla_transform kept varM) trl in
fn varM (f_quant q (cb vsl trl fmla2)) fn varM (f_quant q (f_close_quant vsl trl fmla2))
in in
let fn varM f = fn varM (fmla_transform kept varM f) in let fn varM f = fn varM (fmla_transform kept varM f) in
type_close_select tvs acc fn fmla type_close_select tvs acc fn fmla
......
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