Commit 9a360820 authored by Sylvain Dailler's avatar Sylvain Dailler

Fix crash of eliminate_unknown_types

It was previously possible to keep a constant when there was a removed
symbol in its definition. This changes makes removals be propagated to
other constants.

This patch mainly adds a variable that keeps track of already removed
declarations.
parent e506d384
...@@ -22,6 +22,7 @@ Transformations ...@@ -22,6 +22,7 @@ Transformations
applying hypothesis with nested let-bindings :x: applying hypothesis with nested let-bindings :x:
* Adding arguments to transformations without arguments is now forbidden * Adding arguments to transformations without arguments is now forbidden
(previously ignored):x: (previously ignored):x:
* Fix crash of eliminate_unknown_types
Counterexamples Counterexamples
* Improved display of counterexamples in Task view * Improved display of counterexamples in Task view
......
...@@ -17,13 +17,13 @@ open Ty ...@@ -17,13 +17,13 @@ open Ty
let debug = Debug.register_info_flag "eliminate_unknown_types" let debug = Debug.register_info_flag "eliminate_unknown_types"
~desc:"Print@ debugging@ messages@ of@ the@ eliminate_unknown_types@ transformation." ~desc:"Print@ debugging@ messages@ of@ the@ eliminate_unknown_types@ transformation."
let syntactic_transform transf = let syntactic_transform =
Trans.on_meta Printer.meta_syntax_type (fun metas -> Trans.on_meta Printer.meta_syntax_type (fun metas ->
let symbols = List.fold_left (fun acc meta_arg -> let symbols = List.fold_left (fun acc meta_arg ->
match meta_arg with match meta_arg with
| [MAts ts; MAstr _; MAint _] -> Sts.add ts acc | [MAts ts; MAstr _; MAint _] -> Sts.add ts acc
| _ -> assert false) Sts.empty metas in | _ -> assert false) Sts.empty metas in
transf (fun ts -> Sts.exists (ts_equal ts) symbols)) Trans.return (fun ts -> Sts.exists (ts_equal ts) symbols))
let remove_terms keep = let remove_terms keep =
let keep_ls ls = let keep_ls ls =
...@@ -44,35 +44,56 @@ let remove_terms keep = ...@@ -44,35 +44,56 @@ let remove_terms keep =
| None -> true | None -> true
end end
in in
Trans.decl (fun d -> (* let already_removed = ref Sls.empty in*)
match d.d_node with let is_removed already_removed =
| Dtype ty when not (keep ty) -> Term.t_fold (fun acc t ->
if Debug.test_flag debug then match t.t_node with
Format.printf "remove@ type@ %a@." Pretty.print_ty_decl ty; | Tapp (ls, _) -> Sls.mem ls already_removed || acc
[] | _ -> acc) false
| Ddata l when List.exists (fun (t,_) -> not (keep t)) l -> in
if Debug.test_flag debug then
Format.printf "remove@ data@ %a@." Pretty.print_data_decl (List.hd l); Trans.fold (fun hd (already_removed, task_uc) ->
[] match hd.Task.task_decl.td_node with
| Dparam l when not (keep_ls l) -> | Decl d ->
if Debug.test_flag debug then begin match d.d_node with
Format.printf "remove@ param@ %a@." Pretty.print_ls l; | Dtype ty when not (keep ty) ->
[] Debug.dprintf debug "remove@ type@ %a@." Pretty.print_ty_decl ty;
| Dlogic l when List.exists (fun (l,_) -> not (keep_ls l)) l -> (already_removed, task_uc)
if Debug.test_flag debug then | Ddata l when List.exists (fun (t,_) -> not (keep t)) l ->
Format.printf "remove@ logic@ %a@." Pretty.print_logic_decl (List.hd l); Debug.dprintf debug "remove@ data@ %a@." Pretty.print_data_decl (List.hd l);
[] (already_removed, task_uc)
| Dprop (Pgoal,pr,t) when not (keep_term t) -> | Dparam l when not (keep_ls l) ->
if Debug.test_flag debug then let already_removed = Sls.add l already_removed in
Format.printf "change@ goal@ %a@." Pretty.print_term t; Debug.dprintf debug "remove@ param@ %a@." Pretty.print_ls l;
[create_prop_decl Pgoal pr t_false] (already_removed, task_uc)
| Dprop (_,_,t) when not (keep_term t) -> | Dlogic l when
if Debug.test_flag debug then List.exists (fun (l,def) -> not (keep_ls l) ||
Format.printf "remove@ prop@ %a@." Pretty.print_term t; let (_, t) = open_ls_defn def in
[] not (keep_term t) || is_removed already_removed t) l ->
| _ -> [d]) let already_removed =
None List.fold_left (fun acc (ls, _) -> Sls.add ls acc) already_removed l
in
Debug.dprintf debug "remove@ logic@ %a@." Pretty.print_logic_decl (List.hd l);
(already_removed, task_uc)
| Dprop (Pgoal,pr,t) when not (keep_term t) || is_removed already_removed t ->
Debug.dprintf debug "change@ goal@ %a@." Pretty.print_term t;
let task_uc =
Task.add_decl task_uc (create_prop_decl Pgoal pr t_false) in
(already_removed, task_uc)
| Dprop (_,_,t) when not (keep_term t) || is_removed already_removed t ->
Debug.dprintf debug "remove@ prop@ %a@." Pretty.print_term t;
(already_removed, task_uc)
| _ -> (already_removed, Task.add_decl task_uc d)
end
| _ -> (already_removed, Task.add_tdecl task_uc hd.Task.task_decl)
)
(Sls.empty, None)
let remove_types =
(* TODO fix the pair *)
Trans.bind (Trans.bind syntactic_transform remove_terms)
(fun (_, task) -> Trans.return task)
let () = let () =
Trans.register_transform "eliminate_unknown_types" (syntactic_transform remove_terms) Trans.register_transform "eliminate_unknown_types" remove_types
~desc:"Remove@ types@ unknown@ to@ the@ prover@ and@ terms@ referring@ to@ them@." ~desc:"Remove@ types@ unknown@ to@ the@ prover@ and@ terms@ referring@ to@ them@."
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