Commit de46b1a1 authored by Andrei Paskevich's avatar Andrei Paskevich

Encoding_select: fix selection for the "lskept" and "lsinst" sets

lskept: the old selection check required at least one non-variable
non-closed type in the lsymbol's signature. This is too permissive,
because (list_match : list 'a -> 'b -> 'b) is allowed and will produce
an instance for every type in the "inst" set. The new check requires
that all freely standing type variables occur under a type constructor
elsewhere in the lsymbol's signature.

lsinst: accept any monomorphic instance of any polymorphic symbol
except equality. The old procedure applied the same restrictions
as for the "lskept" set which serve no real purpose for "lsinst".
parent 94b2b33b
......@@ -25,18 +25,11 @@ let register pr none goal all =
(** {2 select Kept} *)
let good_for_inst ls =
let check ty = match ty.ty_node with
| Tyvar _ -> false
| _ -> not (ty_closed ty) in
List.exists check (oty_cons ls.ls_args ls.ls_value)
let trans_on_goal fn = Trans.store (function
| Some { task_decl = { td_node = Decl { d_node = Dprop (_,_,f) }}} -> fn f
| _ -> assert false)
module Kept = struct
(* we ignore the type of the result as we are
only interested in application arguments *)
let add_kept sty _ls tyl _tyv =
......@@ -57,12 +50,23 @@ module Kept = struct
let () = register ft_select_inst kept_none kept_goal kept_all
end
(** {2 select Lskept} *)
module Lskept = struct
let add_lskept sls ls = if good_for_inst ls then Sls.add ls sls else sls
let add_lskept sls ls =
(* We require that every freely standing type variable occurs
under a type constructor elsewhere in the lsymbol's signature.
Thus we bound the (lskept * inst) product and avoid explosion. *)
let ls_sig = oty_cons ls.ls_args ls.ls_value in
let add_ty_t s ty = match ty.ty_node with
| Tyapp _ -> ty_freevars s ty | _ -> s in
let ls_tvs_t = List.fold_left add_ty_t Stv.empty ls_sig in
if Stv.is_empty ls_tvs_t then sls else
let add_ty_v s ty = match ty.ty_node with
| Tyvar v -> Stv.add v s | _ -> s in
let ls_tvs_v = List.fold_left add_ty_v Stv.empty ls_sig in
if Stv.subset ls_tvs_v ls_tvs_t then Sls.add ls sls else sls
let all_lskept task sls = match task.task_decl.td_node with
| Decl { d_node = Dparam ls } ->
......@@ -80,13 +84,15 @@ module Lskept = struct
let () = register ft_select_lskept lskept_none lskept_goal lskept_all
end
(** {2 select Lsinst} *)
module Lsinst = struct
(** TODO : only closed instantiation? without variables? *)
let add_lsinst mls ls tyl tyv =
if good_for_inst ls then Lsmap.add ls tyl tyv mls else mls
if ls_equal ls ps_equ ||
List.for_all ty_closed (oty_cons ls.ls_args ls.ls_value) &&
List.exists (fun ty -> not (ty_closed ty)) (oty_cons tyl tyv)
then mls else Lsmap.add ls tyl tyv mls
let add_lsinst mls t = t_app_fold add_lsinst mls t
......@@ -100,9 +106,3 @@ module Lsinst = struct
let () = register ft_select_lsinst lsinst_none lsinst_goal lsinst_all
end
(*
Local Variables:
compile-command: "unset LANG; make -j -C ../.. byte"
End:
*)
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