Commit f9355bc5 authored by Andrei Paskevich's avatar Andrei Paskevich

correctly determine and protect finite types for tptp encoding

parent ab8fb3d6
......@@ -125,8 +125,8 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
inlining split_goal \
eliminate_definition eliminate_algebraic \
eliminate_inductive eliminate_let eliminate_if \
encoding_enumeration encoding libencoding \
discriminate encoding_select \
libencoding discriminate protect_enumeration \
encoding encoding_select \
encoding_decorate encoding_bridge \
encoding_explicit encoding_guard encoding_sort \
encoding_instantiate simplify_array filter_trigger \
......
......@@ -693,6 +693,7 @@ let rec check_foundness kn d =
| _ -> ()
let rec ts_extract_pos kn sts ts =
assert (ts.ts_def = None);
if ts_equal ts ts_func then [false;true] else
if ts_equal ts ts_pred then [false] else
if Sts.mem ts sts then List.map Util.ttrue ts.ts_args else
......
......@@ -161,11 +161,9 @@ let map env d = match d.d_node with
let defns,axioms = Ssubst.fold conv_f substs ([],[]) in
ts_of_ls env ls (List.rev_append defns axioms)
| Dlogic _ -> Printer.unsupportedDecl d
"Recursively-defined symbols are not supported, \
run eliminate_recursion"
"Recursively-defined symbols are not supported, run eliminate_recursion"
| Dind _ -> Printer.unsupportedDecl d
"Inductive predicates are not supported, \
run eliminate_inductive"
"Inductive predicates are not supported, run eliminate_inductive"
| Dprop (k,pr,f) ->
let substs = ty_quant env f in
let substs_len = Ssubst.cardinal substs in
......@@ -204,7 +202,7 @@ let metas_from_env env =
let fold_inst tyl _ s = List.fold_left (fun s ty -> Sty.add ty s) s tyl in
let fold_ls _ insts s = Mtyl.fold fold_inst insts s in
let sty = Mls.fold fold_ls env Sty.empty in
let add ty decls = create_meta Encoding.meta_kept [MAty ty] :: decls in
let add ty decls = create_meta Libencoding.meta_kept [MAty ty] :: decls in
Sty.fold add sty (Lsmap.metas env)
let lsinst_completion kept lskept env =
......@@ -265,9 +263,9 @@ let lsymbol_distinction =
Trans.decl (map env) None)
let discriminate env = Trans.seq [
Encoding.monomorphise_goal;
Libencoding.monomorphise_goal;
select_lsinst env;
Trans.print_meta Encoding.debug meta_lsinst;
Trans.print_meta Libencoding.debug meta_lsinst;
lsymbol_distinction;
]
......
......@@ -25,7 +25,32 @@ open Decl
open Theory
open Task
let meta_enum = Theory.register_meta "enumeration" [Theory.MTtysymbol]
(* 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 = Theory.register_meta "enumeration_type" [Theory.MTtysymbol]
let meta_phantom =
Theory.register_meta "phantom_type_arg" [Theory.MTtysymbol;Theory.MTint]
let rec enum_ts kn sts ts =
assert (ts.ts_def = None);
if Sts.mem ts sts then raise Exit else
match find_type_definition kn ts with
| Tabstract -> raise Exit
| Talgebraic 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
let enum_ts kn ts = try Some (enum_ts kn Sts.empty ts) with Exit -> None
(** Compile match patterns *)
......@@ -270,7 +295,7 @@ let add_inversion (state,task) ts ty csl =
let task = add_decl task (create_prop_decl Paxiom ax_pr ax_f) in
state, task
let add_type (state,task) ts csl =
let add_type kn (state,task) ts csl =
(* declare constructors as abstract functions *)
let cs_add tsk cs = add_decl tsk (create_logic_decl [cs, None]) in
let task = List.fold_left cs_add task csl in
......@@ -280,9 +305,19 @@ let add_type (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 tag for enumeration if the type is one *)
let enum = List.for_all (fun ls -> ls.ls_args = []) csl in
let task = if enum then add_meta task meta_enum [MAts ts] else task 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
......@@ -294,7 +329,7 @@ let comp t (state,task) = match t.task_decl.td_node with
(* add needed functions and axioms *)
let add acc (ts,df) = match df with
| Tabstract -> acc
| Talgebraic csl -> add_type acc ts csl
| Talgebraic csl -> add_type t.task_known acc ts csl
in
List.fold_left add (state,task) dl
| Decl d ->
......@@ -312,7 +347,7 @@ let comp t (state,task) = match t.task_decl.td_node with
let rstate,rtask = ref state, ref task in
let add _ (ts,csl) () =
let task = add_ty_decl !rtask [ts,Tabstract] in
let state,task = add_type (!rstate,task) ts csl in
let state,task = add_type t.task_known (!rstate,task) ts csl in
rstate := state ; rtask := task ; None
in
let tp_map = Mid.diff add state.tp_map d.d_syms in
......
......@@ -19,4 +19,8 @@
val compile_match : Task.task Trans.trans
val meta_enum : Theory.meta
(* a type constructor tagged "enumeration" generates a finite type
if and only if all of its non-phantom arguments are finite types *)
val meta_enum : Theory.meta (* [MTtysymbol] *)
val meta_phantom : Theory.meta (* [MTtysymbol; MTint] *)
......@@ -26,10 +26,6 @@ open Theory
open Task
open Trans
let debug = Debug.register_flag "encoding"
let meta_kept = register_meta "encoding : kept" [MTty]
let meta_select_kept = register_meta_excl "select_kept" [MTstring]
let meta_enco_kept = register_meta_excl "enco_kept" [MTstring]
let meta_enco_poly = register_meta_excl "enco_poly" [MTstring]
......@@ -46,41 +42,29 @@ let ft_select_kept = ((Hashtbl.create 17) : (Env.env,Sty.t) Trans.flag_trans)
let ft_enco_kept = ((Hashtbl.create 17) : (Env.env,task) Trans.flag_trans)
let ft_enco_poly = ((Hashtbl.create 17) : (Env.env,task) Trans.flag_trans)
let monomorphise_goal = Trans.goal (fun pr f ->
let stv = t_ty_freevars Stv.empty f in
if Stv.is_empty stv then [create_prop_decl Pgoal pr f] else
let mty,ltv = Stv.fold (fun tv (mty,ltv) ->
let ts = create_tysymbol (id_clone tv.tv_name) [] None in
Mtv.add tv (ty_app ts []) mty, ts::ltv) stv (Mtv.empty,[]) in
let f = t_ty_subst mty Mvs.empty f in
List.fold_left
(fun acc ts -> create_ty_decl [ts,Tabstract] :: acc)
[create_prop_decl Pgoal pr f] ltv)
let select_kept def env =
let select = Trans.on_flag meta_select_kept ft_select_kept def env in
let trans task =
let sty = Trans.apply select task in
let create_meta_ty ty = create_meta meta_kept [MAty ty] in
let decls = Sty.fold (flip $ cons create_meta_ty) sty [] in
let add ty acc = create_meta Libencoding.meta_kept [MAty ty] :: acc in
let decls = Sty.fold add (Trans.apply select task) [] in
Trans.apply (Trans.add_tdecls decls) task
in
Trans.store trans
let encoding_smt env = Trans.seq [
monomorphise_goal;
Libencoding.monomorphise_goal;
select_kept def_enco_select_smt env;
Trans.print_meta debug meta_kept;
Trans.print_meta Libencoding.debug Libencoding.meta_kept;
Trans.on_flag meta_enco_kept ft_enco_kept def_enco_kept_smt env;
Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_smt env]
let encoding_tptp env = Trans.seq [
monomorphise_goal;
Libencoding.monomorphise_goal;
select_kept def_enco_select_tptp env;
Trans.print_meta debug meta_kept;
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;
Encoding_enumeration.encoding_enumeration]
Protect_enumeration.protect_enumeration]
let () = register_env_transform "encoding_smt" encoding_smt
let () = register_env_transform "encoding_tptp" encoding_tptp
......
......@@ -17,16 +17,10 @@
(* *)
(**************************************************************************)
val debug : Debug.flag
val meta_kept : Theory.meta
val ft_select_kept : (Env.env,Ty.Sty.t) Trans.flag_trans
val ft_enco_kept : (Env.env,Task.task) Trans.flag_trans
val ft_enco_poly : (Env.env,Task.task) Trans.flag_trans
val monomorphise_goal : Task.task Trans.trans
val encoding_smt : Env.env -> Task.task Trans.trans
val encoding_tptp : Env.env -> Task.task Trans.trans
......@@ -248,7 +248,7 @@ let decl tenv d =
let t env =
Trans.compose Libencoding.close_kept
(Trans.on_tagged_ty meta_kept (fun s ->
(Trans.on_tagged_ty Libencoding.meta_kept (fun s ->
let init_task,tenv = load_prelude s env in
Trans.decl (decl tenv) init_task))
......
......@@ -97,7 +97,7 @@ let mono kept =
let kept = Sty.add ty_type kept in
Trans.decl (d_monomorph kept (lsmap kept)) mono_init
let t = Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
let t = Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
Trans.compose (deco kept) (mono kept))
let () = Hashtbl.replace Encoding.ft_enco_poly "decorate" (const t)
......
......@@ -126,16 +126,17 @@ let decl d = match d.d_node with
let explicit = Trans.decl decl (Task.add_decl None d_ts_type)
let meta_enum = Eliminate_algebraic.meta_enum
let explicit =
Trans.on_tagged_ts meta_enum (fun enum ->
Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
Trans.on_tagged_ts Eliminate_algebraic.meta_enum (fun enum ->
let check ts = 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
"explicit is unsound in presence of type")
"explicit is unsound in presence of type"))
(** {2 monomorphise task } *)
......@@ -152,7 +153,7 @@ let lsmap kept = Wls.memoize 63 (fun ls ->
let d_ts_base = create_ty_decl [ts_base, Tabstract]
let monomorph = Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
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))
......
......@@ -254,7 +254,7 @@ let empty_th =
task
let guard =
Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
Trans.decl (decl kept) empty_th)
(** {2 monomorphise task } *)
......@@ -271,7 +271,7 @@ let lsmap kept = Wls.memoize 63 (fun ls ->
let d_ts_base = create_ty_decl [ts_base, Tabstract]
let monomorph = Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
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))
......
......@@ -531,7 +531,7 @@ let create_trans_complete kept complete =
let encoding_instantiate =
Trans.compose Libencoding.close_kept
(Trans.on_tagged_ty meta_kept (fun kept ->
(Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
Trans.on_meta_excl meta_complete (fun complete ->
create_trans_complete kept complete)))
......@@ -549,7 +549,7 @@ let create_trans_complete create_env kept complete =
Trans.fold_map fold_map env init_task
let t create_env =
Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
Trans.on_meta_excl meta_complete (fun complete ->
create_trans_complete create_env kept complete))
......
......@@ -22,6 +22,12 @@ open Ident
open Ty
open Term
open Decl
open Theory
let debug = Debug.register_flag "encoding"
(* meta to tag the protected types *)
let meta_kept = register_meta "encoding : kept" [MTty]
(* sort symbol of the "universal" type *)
let ts_base = create_tysymbol (id_fresh "uni") [] None
......@@ -90,7 +96,6 @@ let ls_selects_def_of_ts acc ts =
let add acc fs = create_logic_decl [fs,None] :: acc in
List.fold_left add props ls_selects
(* convert a type to a term of type ty_type *)
let rec term_of_ty tvmap ty = match ty.ty_node with
| Tyvar tv ->
......@@ -118,8 +123,6 @@ let lsdecl_of_tydecl acc td = match td with
| { ts_def = Some _ }, _ -> acc
| ts, _ -> create_logic_decl [ls_of_ts ts, None] :: acc
(* convert a type declaration to a list of lsymbol declarations *)
let lsdecl_of_tydecl_select tdl =
let add acc td = match td with
......@@ -237,20 +240,30 @@ let d_monomorph kept lsmap d =
let add ls acc = create_logic_decl [ls,None] :: acc in
Sls.fold add !consts dl
(** close by subterm *)
(* replace type variables in a goal with fresh type constants *)
let monomorphise_goal = Trans.goal (fun pr f ->
let stv = t_ty_freevars Stv.empty f in
if Stv.is_empty stv then [create_prop_decl Pgoal pr f] else
let mty,ltv = Stv.fold (fun tv (mty,ltv) ->
let ts = create_tysymbol (id_clone tv.tv_name) [] None in
Mtv.add tv (ty_app ts []) mty, ts::ltv) stv (Mtv.empty,[]) in
let f = t_ty_subst mty Mvs.empty f in
List.fold_left
(fun acc ts -> create_ty_decl [ts,Tabstract] :: acc)
[create_prop_decl Pgoal pr f] ltv)
(* close by subtype the set of types tagged by meta_kept *)
let close_kept =
Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
let fold ty acc =
let rec add acc ty = ty_fold add (Sty.add ty acc) ty in
add acc ty in
let kept' = Sty.fold fold kept kept in
Trans.on_tagged_ty meta_kept (fun kept ->
let rec add acc ty = ty_fold add (Sty.add ty acc) ty in
let kept' = Sty.fold (Util.flip add) kept kept in
if kept == kept' then Trans.identity
else
let kept' = Sty.diff kept' kept in
let fold ty acc =
Theory.create_meta Encoding.meta_kept [Theory.MAty ty] :: acc in
let fold ty acc = create_meta meta_kept [MAty ty] :: acc in
Trans.add_tdecls (Sty.fold fold kept' []))
(* reconstruct a definition of an lsymbol or make a defining axiom *)
let defn_or_axiom ls f =
match Decl.ls_defn_of_axiom f with
| Some ld -> [create_logic_decl [ld]]
......
......@@ -21,6 +21,11 @@ open Ty
open Term
open Decl
val debug : Debug.flag
(* meta to tag the protected types *)
val meta_kept : Theory.meta
(* sort symbol of the "universal" type *)
val ts_base : tysymbol
......@@ -66,7 +71,10 @@ val lsdecl_of_tydecl_select : ty_decl list -> decl list
(* monomorphise wrt the set of kept types, and a symbol map *)
val d_monomorph : Sty.t -> (lsymbol -> lsymbol) -> decl -> decl list
(* close by subtype the set of type tagged by the meta "kept" *)
(* replace type variables in a goal with fresh type constants *)
val monomorphise_goal : Task.task Trans.trans
(* close by subtype the set of types tagged by meta_kept *)
val close_kept : Task.task Trans.trans
(* reconstruct a definition of an lsymbol or make a defining axiom *)
......
......@@ -26,75 +26,73 @@ open Theory
open Task
open Decl
let meta_enum = Eliminate_algebraic.meta_enum
let protect tenv hls t =
try
let ty = t_type t in
let fs = Mty.find ty tenv in
Hls.replace hls fs ();
fs_app fs [t] ty
with
| Not_found -> t
type tenv = {
enum : Sts.t;
projs : lsymbol Hts.t
}
let add_proj tenv ts =
try Hts.find tenv.projs ts with Not_found ->
let id = id_fresh ("enum_proj_" ^ ts.ts_name.id_string) in
let ty = ty_app ts (List.map ty_var ts.ts_args) in
let fs = create_fsymbol id [ty] ty in
Hts.add tenv.projs ts fs;
fs
let proj tenv t ty = match ty.ty_node with
| Tyapp (ts,_) when Sts.mem ts tenv.enum ->
let fs = Hts.find tenv.projs ts in
t_app fs [t] t.t_ty
| _ when ty_s_any (fun ts -> Sts.mem ts tenv.enum) (t_type t) ->
Printer.unsupportedType ty "complexe finite type"
| _ -> t
let proj tenv t = match t.t_node with
| Tapp (ls,_) ->
proj tenv t (of_option ls.ls_value)
| Tvar _ | Tconst _ | Teps _ ->
proj tenv t (t_type t)
| Tif _ | Tcase _ | Tlet _ ->
t
| Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
let rec rewrite_term tenv t = match t.t_node with
let rec rewrite_term tenv hls t = match t.t_node with
| Tapp (fs,tl) ->
let pin t = proj tenv (rewrite_term tenv t) in
let pin t = protect tenv hls (rewrite_term tenv hls t) in
t_app fs (List.map pin tl) t.t_ty
| Tcase _ ->
Printer.unsupportedTerm t "use eliminate_algebraic"
| _ -> TermTF.t_map (rewrite_term tenv) (rewrite_fmla tenv) t
and rewrite_fmla tenv f = match f.t_node with
| Tapp (ps,tl) ->
let pin t = proj tenv (rewrite_term tenv t) in
ps_app ps (List.map pin tl)
| Tcase _ ->
Printer.unsupportedTerm f "use eliminate_algebraic"
| _ -> TermTF.t_map (rewrite_term tenv) (rewrite_fmla tenv) f
| _ -> t_map (rewrite_term tenv hls) t
let decl tenv d = match d.d_node with
| Dtype tl ->
let add acc t = match t with
| ts, Tabstract when Sts.mem ts tenv.enum ->
let ls = add_proj tenv ts in
let acc = create_ty_decl [t] :: acc in
create_logic_decl [ls, None] :: acc
| _, Tabstract ->
create_ty_decl [t] :: acc
| _ ->
Printer.unsupportedDecl d "use eliminate_algebraic"
in
List.rev (List.fold_left add [] tl)
| Dtype [_,Tabstract] -> [d]
| Dtype _ -> Printer.unsupportedDecl d
"Algebraic and recursively-defined types are \
not supported, run eliminate_algebraic"
| Dlogic [_, None] -> [d]
| Dlogic [ls, Some ld] when not (Sid.mem ls.ls_name d.d_syms) ->
let hls = Hls.create 7 in
let f = rewrite_term tenv hls (ls_defn_axiom ld) in
let decl fs () decls = create_logic_decl [fs,None] :: decls in
Hls.fold decl hls (Libencoding.defn_or_axiom ls f)
| Dlogic _ -> Printer.unsupportedDecl d
"Recursively-defined symbols are not supported, run eliminate_recursion"
| Dind _ -> Printer.unsupportedDecl d
"Inductive predicates are not supported, run eliminate_inductive"
| _ ->
[DeclTF.decl_map (rewrite_term tenv) (rewrite_fmla tenv) d]
let encoding_enumeration =
let projs = Hts.create 17 in
Trans.on_tagged_ts meta_enum (fun enum ->
let tenv = { enum = enum ; projs = projs } in
Trans.decl (decl tenv) None)
let hls = Hls.create 7 in
let d = decl_map (rewrite_term tenv hls) d in
let decl fs () decls = create_logic_decl [fs,None] :: decls in
Hls.fold decl hls [d]
let () = Trans.register_transform "encoding_enumeration" encoding_enumeration
let protect_enumeration =
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 add_ph phmap = 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
| _ -> 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
in
let add_protect ty tenv =
if not (finite_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 fs = create_fsymbol id [ty] ty in
Mty.add ty fs tenv
in
let tenv = Sty.fold add_protect kept Mty.empty in
Trans.decl (decl tenv) None)))
......@@ -17,4 +17,4 @@
(* *)
(**************************************************************************)
val encoding_enumeration : Task.task Trans.trans
val protect_enumeration : 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