Commit 629d464c authored by Andrei Paskevich's avatar Andrei Paskevich

treat abstract types as potentially finite, to avoid unsoundness

parent 8704af6f
......@@ -129,7 +129,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
inlining split_goal induction \
eliminate_definition eliminate_algebraic \
eliminate_inductive eliminate_let eliminate_if \
libencoding discriminate protect_enumeration \
libencoding discriminate protect_finite \
encoding encoding_select \
encoding_decorate encoding_decoexp encoding_twin \
encoding_explicit encoding_guard encoding_sort \
......
......@@ -26,53 +26,34 @@ open Decl
open Theory
open Task
(* a type constructor tagged "enumeration" generates a finite type
if and only if all of its non-phantom arguments are finite types *)
let meta_enum = register_meta "enumeration_type" [MTtysymbol]
let meta_phantom = register_meta "phantom_type_arg" [MTtysymbol;MTint]
let rec enum_ts kn sts ts =
assert (ts.ts_def = None);
if Sts.mem ts sts then raise Exit else
match find_constructors kn ts with
| [] -> raise Exit
| csl ->
let sts = Sts.add ts sts in
let rec finite_ty stv ty = match ty.ty_node with
| Tyvar tv -> Stv.add tv stv
| Tyapp (ts,tl) ->
let check acc ph ty = if ph then acc else finite_ty acc ty in
List.fold_left2 check stv (enum_ts kn sts ts) tl
in
let check_cs acc (ls,_) = List.fold_left finite_ty acc ls.ls_args in
let stv = List.fold_left check_cs Stv.empty csl in
List.map (fun v -> not (Stv.mem v stv)) ts.ts_args
(* a type constructor generates an infinite type if either it is tagged by
meta_infinite or one of its "material" arguments is an infinite type *)
let enum_ts kn ts = try Some (enum_ts kn Sts.empty ts) with Exit -> None
let meta_infinite = register_meta "infinite_type" [MTtysymbol]
let meta_material = register_meta "material_type_arg" [MTtysymbol;MTint]
let is_finite_ty enum phlist =
let add_ph phmap = function
let get_material_args matl =
let add_arg acc = function
| [MAts ts; MAint i] ->
let phmap, pha = try phmap, Mts.find ts phmap with
| Not_found ->
let pha = Array.make (List.length ts.ts_args) false in
Mts.add ts pha phmap, pha
in
Array.set pha i true;
phmap
let acc, mat = try acc, Mts.find ts acc with Not_found ->
let mat = Array.make (List.length ts.ts_args) false in
Mts.add ts mat acc, mat in
Array.set mat i true;
acc
| _ -> assert false
in
let phmap = List.fold_left add_ph Mts.empty phlist in
let phmap = Mts.map Array.to_list phmap in
let rec finite_ty ty = match ty.ty_node with
| Tyapp (ts,tl) when Mts.mem ts enum ->
let phl = try Mts.find ts phmap with Not_found ->
List.map Util.ffalse ts.ts_args in
List.for_all2 (fun ph ty -> ph || finite_ty ty) phl tl
| _ -> false
Mts.map Array.to_list (List.fold_left add_arg Mts.empty matl)
let is_infinite_ty inf_ts ma_map =
let rec inf_ty ty = match ty.ty_node with
| Tyapp (ts,_) when Mts.mem ts inf_ts -> true
| Tyapp (ts,_) when not (Mts.mem ts ma_map) -> false
| Tyapp (ts,l) ->
let mat = Mts.find ts ma_map in
List.exists2 (fun mat ty -> mat && inf_ty ty) mat l
| _ -> false (* FIXME? can we have non-ground types here? *)
in
finite_ty
inf_ty
(** Compile match patterns *)
......@@ -99,6 +80,8 @@ type state = {
mt_map : lsymbol Mts.t; (* from type symbols to selector functions *)
pj_map : lsymbol list Mls.t; (* from constructors to projections *)
tp_map : decl Mid.t; (* skipped tuple symbols *)
inf_ts : Sts.t; (* infinite types *)
ma_map : bool list Mts.t; (* material type arguments *)
keep_t : bool; (* keep algebraic type definitions *)
keep_e : bool; (* keep monomorphic enumeration types *)
keep_r : bool; (* keep non-recursive records *)
......@@ -109,6 +92,8 @@ let empty_state = {
mt_map = Mts.empty;
pj_map = Mls.empty;
tp_map = Mid.empty;
inf_ts = Sts.add ts_real (Sts.singleton ts_int);
ma_map = Mts.empty;
keep_t = false;
keep_e = false;
keep_r = false;
......@@ -336,7 +321,7 @@ let add_inversion (state,task) ts ty csl =
let ax_f = t_forall_close [ax_vs] [] ax_f in
state, add_prop_decl task Paxiom ax_pr ax_f
let add_type kn (state,task) ts csl =
let add_type (state,task) (ts,csl) =
(* declare constructors as abstract functions *)
let cs_add tsk (cs,_) = add_param_decl tsk cs in
let task =
......@@ -347,22 +332,35 @@ let add_type kn (state,task) ts csl =
let state,task = add_indexer (state,task) ts ty csl in
let state,task = add_projections (state,task) ts ty csl in
let state,task = add_inversion (state,task) ts ty csl in
(* add the tags for enumeration if the type is one *)
let task = match enum_ts kn ts with
| None -> task
| Some phs ->
let task = add_meta task meta_enum [MAts ts] in
let cpt = ref (-1) in
let add task ph =
incr cpt;
if ph then
add_meta task meta_phantom [MAts ts; MAint !cpt]
else task in
List.fold_left add task phs
in
(* return the updated state and task *)
state, task
let add_tags mts (state,task) (ts,csl) =
let rec mat_ts sts ts csl =
let sts = Sts.add ts sts in
let add s (ls,_) = List.fold_left (mat_ty sts) s ls.ls_args in
let stv = List.fold_left add Stv.empty csl in
List.map (fun v -> Stv.mem v stv) ts.ts_args
and mat_ty sts stv ty = match ty.ty_node with
| Tyvar tv -> Stv.add tv stv
| Tyapp (ts,tl) ->
if Sts.mem ts sts then raise Exit; (* infinite type *)
let matl = try Mts.find ts state.ma_map with
Not_found -> mat_ts sts ts (Mts.find_def [] ts mts) in
let add s mat ty = if mat then mat_ty sts s ty else s in
List.fold_left2 add stv matl tl
in try
let matl = mat_ts state.inf_ts ts csl in
let state = { state with ma_map = Mts.add ts matl state.ma_map } in
let c = ref (-1) in
let add_material task m =
incr c;
if m then add_meta task meta_material [MAts ts; MAint !c] else task
in
state, List.fold_left add_material task matl
with Exit ->
let state = { state with inf_ts = Sts.add ts state.inf_ts } in
state, add_meta task meta_infinite [MAts ts]
let comp t (state,task) = match t.task_decl.td_node with
| Decl { d_node = Ddata dl } ->
(* add type declarations *)
......@@ -373,12 +371,25 @@ let comp t (state,task) = match t.task_decl.td_node with
else List.fold_left (fun t (ts,_) -> add_ty_decl t ts) task dl
in
(* add needed functions and axioms *)
let add acc (ts,csl) = add_type t.task_known acc ts csl in
List.fold_left add (state,task) dl
let state, task = List.fold_left add_type (state,task) dl in
(* add the tags for infitite types and material arguments *)
let mts = List.fold_right (fun (t,l) -> Mts.add t l) dl Mts.empty in
let state, task = List.fold_left (add_tags mts) (state,task) dl in
(* return the updated state and task *)
state, task
| Decl d ->
let fnT = rewriteT t.task_known state in
let fnF = rewriteF t.task_known state Svs.empty true in
state, add_decl task (DeclTF.decl_map fnT fnF d)
| Meta (m, [MAts ts]) when meta_equal m meta_infinite ->
let state = { state with inf_ts = Sts.add ts state.inf_ts } in
state, add_tdecl task t.task_decl
| Meta (m, [MAts ts; MAint i]) when meta_equal m meta_material ->
let ma = try Array.of_list (Mts.find ts state.ma_map) with
| Not_found -> Array.make (List.length ts.ts_args) false in
let ml = Array.set ma i true; Array.to_list ma in
let state = { state with ma_map = Mts.add ts ml state.ma_map } in
state, add_tdecl task t.task_decl
| _ ->
state, add_tdecl task t.task_decl
......@@ -417,8 +428,13 @@ let comp t (state,task) = match t.task_decl.td_node with
| _ ->
comp t (state,task)
let eliminate_match = Trans.compose compile_match
(Trans.fold_map comp empty_state None)
let init_task =
let init = Task.add_meta None meta_infinite [MAts ts_int] in
let init = Task.add_meta init meta_infinite [MAts ts_real] in
init
let eliminate_match =
Trans.compose compile_match (Trans.fold_map comp empty_state init_task)
let meta_elim = register_meta "eliminate_algebraic" [MTstring]
......@@ -433,7 +449,7 @@ let eliminate_algebraic = Trans.compose compile_match
| _ -> raise (Invalid_argument "meta eliminate_algebraic")
in
let st = List.fold_left check st ml in
Trans.fold_map comp st None))
Trans.fold_map comp st init_task))
(** Eliminate user-supplied projection functions *)
......
......@@ -23,11 +23,14 @@ val compile_match : Task.task Trans.trans
val meta_proj : Theory.meta (* [MTlsymbol; MTlsymbol; MTint; MTprsymbol] *)
(* projection symbol, constructor symbol, position, defining axiom *)
(* a type constructor tagged "enumeration" generates a finite type
if and only if all of its non-phantom arguments are finite types *)
(* a type constructor generates an infinite type if either it is tagged by
meta_infinite or one of its "material" arguments is an infinite type *)
val meta_enum : Theory.meta (* [MTtysymbol] *)
val meta_phantom : Theory.meta (* [MTtysymbol; MTint] *)
val meta_infinite : Theory.meta (* [MTtysymbol] *)
val meta_material : Theory.meta (* [MTtysymbol; MTint] *)
(* tests whether a type is finite given [meta_enum] and [meta_phantom] *)
val is_finite_ty : Ty.Sts.t -> Theory.meta_arg list list -> (Ty.ty -> bool)
(* extracts the material type arguments from [meta_material] *)
val get_material_args : Theory.meta_arg list list -> bool list Ty.Mts.t
(* tests if a type is infinite given [meta_infinite] and [meta_material] *)
val is_infinite_ty : Ty.Sts.t -> bool list Ty.Mts.t -> (Ty.ty -> bool)
......@@ -65,7 +65,7 @@ let encoding_tptp env = Trans.seq [
Trans.print_meta Libencoding.debug Libencoding.meta_kept;
Trans.on_flag meta_enco_kept ft_enco_kept def_enco_kept_tptp env;
Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_tptp env;
Protect_enumeration.protect_enumeration]
Protect_finite.protect_finite]
let () = register_env_transform "encoding_smt" encoding_smt
let () = register_env_transform "encoding_tptp" encoding_tptp
......
......@@ -72,9 +72,9 @@ let deco_term kept tvar =
let ls_inf_type = create_psymbol (id_fresh "infinite") [ty_type]
let deco_decl kept enum phmap d = match d.d_node with
let deco_decl kept inf_ts ma_map d = match d.d_node with
| Dtype { ts_def = Some _ } -> []
| Dtype ts when not (Mts.mem ts enum) ->
| Dtype ts when Mts.mem ts inf_ts ->
let ls = ls_of_ts ts in
let vs_of_tv v = create_vsymbol (id_clone v.tv_name) ty_type in
let vl = List.map vs_of_tv ts.ts_args in
......@@ -97,15 +97,15 @@ let deco_decl kept enum phmap d = match d.d_node with
let vs_of_tv v = create_vsymbol (id_clone v.tv_name) ty_type in
let vl = List.map vs_of_tv ts.ts_args in
let t = fs_app ls (List.map t_var vl) ty_type in
let phl = try Mts.find ts phmap with Not_found ->
List.map Util.ffalse ts.ts_args in
let add ph v l = if ph then l else
let add mat v l = if not mat then l else
let id = id_fresh ("Inf_ts_" ^ ts.ts_name.id_string) in
let f = ps_app ls_inf_type [t] in
let h = ps_app ls_inf_type [t_var v] in
let f = t_forall_close vl [] (t_implies h f) in
create_prop_decl Paxiom (create_prsymbol id) f :: l in
let inf_tss = List.fold_right2 add phl vl [] in
let inf_tss =
try List.fold_right2 add (Mts.find ts ma_map) vl []
with Not_found -> [] in
[d; lsdecl_of_ts ts] @ inf_tss
| Ddata _ -> Printer.unsupportedDecl d
"Algebraic and recursively-defined types are \
......@@ -141,22 +141,10 @@ let deco_init =
init
let deco kept =
Trans.on_tagged_ts Eliminate_algebraic.meta_enum (fun enum ->
Trans.on_meta Eliminate_algebraic.meta_phantom (fun phlist ->
let add_ph phmap = function
| [Theory.MAts ts; Theory.MAint i] ->
let phmap, pha = try phmap, Mts.find ts phmap with
| Not_found ->
let pha = Array.make (List.length ts.ts_args) false in
Mts.add ts pha phmap, pha
in
Array.set pha i true;
phmap
| _ -> assert false
in
let phmap = List.fold_left add_ph Mts.empty phlist in
let phmap = Mts.map Array.to_list phmap in
Trans.decl (deco_decl kept enum phmap) deco_init))
Trans.on_tagged_ts Eliminate_algebraic.meta_infinite (fun infts ->
Trans.on_meta Eliminate_algebraic.meta_material (fun matl ->
let ma_map = Eliminate_algebraic.get_material_args matl in
Trans.decl (deco_decl kept infts ma_map) deco_init))
(** Monomorphisation *)
......@@ -175,9 +163,7 @@ let lsmap kept = Wls.memoize 63 (fun ls ->
&& List.for_all2 ty_equal tyl ls.ls_args then ls
else create_lsymbol (id_clone ls.ls_name) tyl tyr)
let mono_init =
let init = Task.add_ty_decl None ts_base in
init
let mono_init = Task.add_decl None d_ts_base
let mono kept =
let kept = Sty.add ty_type kept in
......
......@@ -105,7 +105,6 @@ let lsmap kept = Wls.memoize 63 (fun ls ->
&& List.for_all2 ty_equal tyl ls.ls_args then ls
else create_lsymbol (id_clone ls.ls_name) tyl tyr)
let d_ts_base = create_ty_decl ts_base
let d_ts_deco = create_ty_decl ts_deco
let mono_init =
......
......@@ -131,19 +131,6 @@ let decl d = match d.d_node with
let explicit = Trans.decl decl (Task.add_decl None d_ts_type)
let explicit =
Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
Trans.on_tagged_ts Eliminate_algebraic.meta_enum (fun enum ->
let check ts = not (ts.ts_args = [] && Sty.mem (ty_app ts []) kept) in
let enum = Sts.filter check enum in
if Sts.is_empty enum then explicit
else
let ts = Sts.choose enum in
let ty = ty_app ts (List.map ty_var ts.ts_args) in
Printer.unsupportedType ty
"Encoding_explicit is unsound in presence of unprotected finite types"))
(** {2 monomorphise task } *)
open Libencoding
......@@ -159,12 +146,14 @@ let lsmap kept = Wls.memoize 63 (fun ls ->
List.for_all2 ty_equal ty_arg ls.ls_args then ls
else create_lsymbol (id_clone ls.ls_name) ty_arg ty_res)
let d_ts_base = create_ty_decl ts_base
let monomorph = Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
let kept = Sty.add ty_type kept in
let decl = d_monomorph kept (lsmap kept) in
Trans.decl decl (Task.add_decl None d_ts_base))
(* This encoding method is unsound in presence of finite types. *)
(*
let () = Hashtbl.replace Encoding.ft_enco_poly "explicit"
(fun _ -> Trans.compose explicit monomorph)
*)
......@@ -260,8 +260,6 @@ let lsmap kept = Wls.memoize 63 (fun ls ->
List.for_all2 ty_equal ty_arg ls.ls_args then ls
else create_lsymbol (id_clone ls.ls_name) ty_arg ty_res)
let d_ts_base = create_ty_decl ts_base
let monomorph = Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
let kept = Sty.add ty_type kept in
let decl = d_monomorph kept (lsmap kept) in
......
......@@ -124,22 +124,4 @@ let decl tenv d =
let t = Trans.on_tagged_ty Libencoding.meta_kept (fun s ->
Trans.decl (decl (Mty.mapi make_pont s)) None)
(* Every finite protected type has a finite twin type. But
as we do not introduce twin types explicitly, we declare
a dummy type constant finite. This is enough to trigger
the safety in Encoding_explicit. *)
let ts_dummy = Ty.create_tysymbol (id_fresh "finite_twin_type") [] None
let enum =
Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
Trans.on_tagged_ts Eliminate_algebraic.meta_enum (fun enum ->
Trans.on_meta Eliminate_algebraic.meta_phantom (fun phlist ->
let finite_ty = Eliminate_algebraic.is_finite_ty enum phlist in
if not (Sty.exists finite_ty kept) then Trans.identity else
Trans.add_tdecls [create_meta Eliminate_algebraic.meta_enum
[MAts ts_dummy]])))
let twin = const (Trans.compose t enum)
let () = Hashtbl.replace Encoding.ft_enco_kept "twin" twin
let () = Hashtbl.replace Encoding.ft_enco_kept "twin" (const t)
......@@ -62,15 +62,16 @@ let decl tenv d = match d.d_node with
let decl fs () decls = create_param_decl fs :: decls in
Hls.fold decl hls [d]
let protect_enumeration =
let protect_finite =
Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
Trans.on_tagged_ts Eliminate_algebraic.meta_enum (fun enum ->
Trans.on_meta Eliminate_algebraic.meta_phantom (fun phlist ->
let finite_ty = Eliminate_algebraic.is_finite_ty enum phlist in
Trans.on_tagged_ts Eliminate_algebraic.meta_infinite (fun infts ->
Trans.on_meta Eliminate_algebraic.meta_material (fun matl ->
let ma_map = Eliminate_algebraic.get_material_args matl in
let inf_ty = Eliminate_algebraic.is_infinite_ty infts ma_map in
let add_protect ty tenv =
if not (finite_ty ty) then tenv else
if inf_ty ty then tenv else
let ts = match ty.ty_node with Tyapp (s,_) -> s | _ -> assert false in
let id = id_fresh ("protect_enum_" ^ ts.ts_name.id_string) in
let id = id_fresh ("protect_finite_" ^ ts.ts_name.id_string) in
let fs = create_fsymbol id [ty] ty in
Mty.add ty fs tenv
in
......
......@@ -18,4 +18,4 @@
(* *)
(**************************************************************************)
val protect_enumeration : Task.task Trans.trans
val protect_finite : Task.task Trans.trans
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