Commit 3695c1f8 authored by Francois Bobot's avatar Francois Bobot
Browse files

split the encoding encoding_bridge encoding_instantiate first part

parent c5184070
......@@ -109,6 +109,7 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
LIB_TRANSFORM = simplify_recursive_definition simplify_formula inlining \
split_conjunction encoding_decorate encoding_decorate_mono \
encoding_bridge\
eliminate_definition eliminate_algebraic \
encoding_enumeration \
eliminate_inductive eliminate_let eliminate_if \
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Util
open Ident
open Ty
open Term
open Task
open Theory
open Task
open Decl
let why_filename = ["transform" ; "encoding_decorate"]
let meta_kept = Encoding_decorate.meta_kept
(* From Encoding Polymorphism CADE07*)
type lconv = {tb2t : lsymbol;
t2tb : lsymbol;
tb : ty}
type tenv = {kept : Sts.t option;
clone_builtin : tysymbol -> Theory.tdecl list;
specials : lconv Hty.t;
trans_lsymbol : lsymbol Hls.t;
trans_tsymbol : tysymbol Hts.t}
(* trans_lsymbol ne depend pour l'instant pas du but,
comme specials_type ne depend pas*)
let load_prelude kept env =
let task = None in
let specials = Hty.create 17 in
let builtin = Env.find_theory env why_filename "Bridge" in
let type_t = Theory.ns_find_ts builtin.th_export ["t"] in
let trans_tsymbol = Hts.create 17 in
let clone_builtin ts =
let task = None in
let name = ts.ts_name.id_string in
let th_uc = create_theory (id_fresh ("bridge_for_"^name)) in
let th_uc =
if ts_equal ts ts_int || ts_equal ts ts_real then th_uc
else Theory.add_ty_decl th_uc [ts,Tabstract] in
let th_inst = create_inst
~ts:[type_t,ts] ~ls:[] ~lemma:[] ~goal:[] in
let th_uc = Theory.clone_export th_uc builtin th_inst in
let th = close_theory th_uc in
let tb2t = ns_find_ls th.th_export ["tb2t"] in
let t2tb = ns_find_ls th.th_export ["t2tb"] in
let tb = ns_find_ts th.th_export ["tb"] in
let lconv = { tb2t = tb2t; t2tb = t2tb; tb = ty_app tb []} in
let task = Task.use_export task th in
Hts.add trans_tsymbol ts tb;
Hty.add specials (ty_app ts []) lconv;
task_tdecls task in
task,
{ kept = kept;
clone_builtin = Wts.memoize 7 clone_builtin;
specials = specials;
trans_lsymbol = Hls.create 17;
trans_tsymbol = trans_tsymbol}
(* Translate a type to a type without kept *)
let rec ty_of_ty tenv ty =
match ty.ty_node with
| Tyapp (ts,l) ->
let tts = try Hts.find tenv.trans_tsymbol ts
with Not_found -> ts in
ty_app tts (List.map (ty_of_ty tenv) l)
| Tyvar _ -> ty
(* Translate with the previous function except when the type is specials *)
let ty_of_ty_specials tenv ty =
if Hty.mem tenv.specials ty then ty else ty_of_ty tenv ty
let is_kept tenv ts =
ts.ts_args = [] &&
begin
match tenv.kept with
| None -> true (* every_simple *)
| Some s -> Sts.mem ts s
end
(* Convert a logic symbols to the encoded one *)
let conv_ls tenv ls =
if ls_equal ls ps_equ
then ls
else
let tyl = List.map (ty_of_ty_specials tenv) ls.ls_args in
let ty_res = Util.option_map (ty_of_ty_specials tenv) ls.ls_value in
if Util.option_eq ty_equal ty_res ls.ls_value
&& List.for_all2 ty_equal tyl ls.ls_args
then ls
else
let preid = id_clone ls.ls_name in
create_lsymbol preid tyl ty_res
(* Convert the argument of a function use the bridge if needed*)
let conv_arg tenv t aty =
let tty = t.t_ty in
if ty_equal tty aty then t else
try
(* tb2t *)
let tylconv = Hty.find tenv.specials aty in
t_app tylconv.tb2t [t] aty
with Not_found ->
try
(* polymorph specials t2tb *)
let tylconv = Hty.find tenv.specials tty in
t_app tylconv.t2tb [t] tylconv.tb
with Not_found ->
(* polymorph not specials *)
t
(* Convert with a bridge an application if needed *)
let conv_res_app tenv p tl tty =
try
(* tty is a special value *)
let tylconv = Hty.find tenv.specials tty in
let vty = Util.of_option p.ls_value in
if ty_equal vty tty then (* vty too *) t_app p tl tty
else
(* p is polymorph *)
let t = t_app p tl tylconv.tb in
t_app tylconv.tb2t [t] tty
with Not_found ->
let tty = ty_of_ty tenv tty in
t_app p tl tty
let rec rewrite_term tenv t =
(*Format.eprintf "@[<hov 2>Term : %a =>@\n@?" Pretty.print_term t;*)
let fnT = rewrite_term tenv in
let fnF = rewrite_fmla tenv in
match t.t_node with
| Tapp(p,tl) ->
let tl = List.map fnT tl in
let p = Hls.find tenv.trans_lsymbol p in
let tl = List.map2 (conv_arg tenv) tl p.ls_args in
conv_res_app tenv p tl t.t_ty
| Tconst _ | Tvar _ | Tif _ | Tlet _ -> t_map fnT fnF t
| Tcase _ | Teps _ | Tbvar _ ->
Printer.unsupportedTerm t
"Encoding decorate : I can't encode this term"
and rewrite_fmla tenv f =
(* Format.eprintf "@[<hov 2>Fmla : %a =>@\n@?" Pretty.print_fmla f; *)
let fnT = rewrite_term tenv in
let fnF = rewrite_fmla tenv in
match f.f_node with
| Fapp(p, tl) when ls_equal p ps_equ ->
let tl = List.map fnT tl in
begin
match tl with
| [a1;_] ->
let ty = a1.t_ty in
let tl = List.map2 (conv_arg tenv) tl [ty;ty] in
f_app p tl
| _ -> assert false
end
| Fapp(p, tl) ->
let tl = List.map fnT tl in
let p = Hls.find tenv.trans_lsymbol p in
let tl = List.map2 (conv_arg tenv) tl p.ls_args in
f_app p tl
| _ -> f_map fnT fnF f
let decl (tenv:tenv) d =
(* let fnT = rewrite_term tenv in *)
let fnF = rewrite_fmla tenv in
match d.d_node with
| Dtype [ts,Tabstract] when is_kept tenv ts ->
tenv.clone_builtin ts
| Dtype [_,Tabstract] -> [create_decl d]
| Dtype _ -> Printer.unsupportedDecl
d "encoding_decorate : I can work only on abstract \
type which are not in recursive bloc."
| Dlogic l ->
let fn = function
| _ls, Some _ ->
Printer.unsupportedDecl
d "encoding_decorate : I can't encode definition. \
Perhaps you could use eliminate_definition"
| ls, None ->
try
let ls = Hls.find tenv.trans_lsymbol ls in
ls,None
with Not_found ->
let ls_conv = conv_ls tenv ls in
Hls.add tenv.trans_lsymbol ls ls_conv;
ls_conv,None in
[create_decl (create_logic_decl (List.map fn l))]
| Dind _ -> Printer.unsupportedDecl
d "encoding_decorate : I can't work on inductive"
(* let fn (pr,f) = pr, fnF f in *)
(* let fn (ps,l) = ps, List.map fn l in *)
(* [create_ind_decl (List.map fn l)] *)
| Dprop (k,pr,f) ->
let f = fnF f in
[create_decl (create_prop_decl k pr f)]
(*
let decl tenv d =
Format.eprintf "@[<hov 2>Decl : %a =>@\n@?" Pretty.print_decl d;
let res = decl tenv d in
Format.eprintf "%a@]@." (Pp.print_list Pp.newline Pretty.print_task_tdecl)
res;
res
*)
let t env = Trans.on_meta meta_kept (fun tds ->
let s = Task.find_tagged_ts meta_kept tds Sts.empty in
let init_task,tenv = load_prelude (Some s) env in
Trans.tdecl (decl tenv) init_task)
let () = Trans.register_env_transform "encoding_bridge" t
let t_all env =
let init_task,tenv = load_prelude None env in
Trans.tdecl (decl tenv) init_task
let () = Trans.register_env_transform "encoding_bridge_every_simple" t_all
......@@ -55,17 +55,18 @@ type tenv_aux = {
}
type tenv =
| Tenv of tenv_aux (* The transformation decorates with tenv_aux.* *)
| No_black_part (* The environnement when the transformation isn't complete*)
| Complete (* The transformation keep the polymorphism *)
| Incomplete (* The environnement when the transformation isn't complete*)
(* A type is projected on term or type depending
of its color (green part,red part, black part) *)
type tty =
| Tyterm of term
| Tyterm of ty
| Tyty of ty
let print_tty fmt = function
| Tyterm term -> Format.fprintf fmt "(Tyterm %a)" Pretty.print_term term
| Tyterm ty -> Format.fprintf fmt "(Tyterm %a)" Pretty.print_ty ty
| Tyty ty -> Format.fprintf fmt "(Tyty %a)" Pretty.print_ty ty
(* It can be backprojected to type, ty_dumb is like a bottom type it
......@@ -74,17 +75,21 @@ let reduce_to_type = function
| Tyty ty -> ty
| Tyterm _ -> ty_dumb
let reduce_to_pos tenv = function
| Tyty ty -> ty
| Tyterm _ -> match tenv with
| No_black_part -> assert false (* All is type in this mode *)
| Tenv tenv -> tenv.undeco
let reduce_to_neg tenv = function
| Tyty ty -> ty
| Tyterm _ -> match tenv with
| No_black_part -> assert false (* All is type in this mode *)
| Tenv tenv -> tenv.deco
let reduce_to_real = function
| Tyty ty | Tyterm ty -> ty
(* let reduce_to_pos tenv = function *)
(* | Tyty ty -> ty *)
(* | Tyterm _ -> match tenv with *)
(* | Incomplete -> assert false (\* All is type in this mode *\) *)
(* | Tenv tenv -> tenv.undeco *)
(* let reduce_to_neg tenv = function *)
(* | Tyty ty -> ty *)
(* | Tyterm _ -> match tenv with *)
(* | Incomplete -> assert false (\* All is type in this mode *\) *)
(* | Tenv tenv -> tenv.deco *)
(* The environnement of the transformation between two decl (* unmutable *) *)
type env = {
......@@ -92,7 +97,7 @@ type env = {
ekeep : Sty.t;
eprojty : ty Mty.t;
edefined_lsymbol : lsymbol Mtyl.t Mls.t;
edefined_tsymbol : lsymbol Mtyl.t Mts.t;
edefined_tsymbol : tysymbol Mtyl.t Mts.t;
}
(* The environnement of the transformation during
......@@ -102,7 +107,7 @@ type menv = {
keep : Sty.t;
mutable projty : ty Mty.t;
mutable defined_lsymbol : lsymbol Mtyl.t Mls.t;
mutable defined_tsymbol : lsymbol Mtyl.t Mts.t;
mutable defined_tsymbol : tysymbol Mtyl.t Mts.t;
mutable undef_lsymbol : Sls.t;
mutable undef_tsymbol : Sts.t;
}
......@@ -117,55 +122,22 @@ let print_env fmt menv =
(Pp.print_iter2 Mts.iter Pp.semi Pp.comma Pretty.print_ts
(Pp.print_iter2 Mtyl.iter Pp.semi Pp.arrow
(Pp.print_list Pp.space Pretty.print_ty)
Pretty.print_ls)) menv.defined_tsymbol
Pretty.print_ts)) menv.defined_tsymbol
type tvar = {
tvar_term : vsymbol Mtv.t;
tvar_ty : ty Mtv.t;
}
type tvar = ty Mtv.t
let why_filename = Encoding_decorate.why_filename
(* Useful function *)
let rec logic_inst tl = function
| None -> List.map reduce_to_type tl
| Some ty -> (reduce_to_type ty) :: (logic_inst tl None)
let find_logic menv p tyl ty =
if ls_equal p ps_equ then p else
let inst = logic_inst tyl ty in
(*Format.eprintf "fl : env : %a p : %a | inst : %a@."
print_env menv
Pretty.print_ls p
(Pp.print_list Pp.comma Pretty.print_ty) inst;*)
try
let insts = Mls.find p menv.defined_lsymbol in
Mtyl.find inst insts
with Not_found ->
let insts =
try
Mls.find p menv.defined_lsymbol
with Not_found ->
Mtyl.empty in
let arg = List.map (reduce_to_neg menv.tenv) tyl in
let result = option_map (reduce_to_pos menv.tenv) ty in
let ls = if List.for_all2 ty_equal arg p.ls_args &&
option_eq ty_equal result p.ls_value
then p else create_lsymbol (id_clone p.ls_name) arg result in
let insts = Mtyl.add inst ls insts in
menv.defined_lsymbol <- Mls.add p insts menv.defined_lsymbol;
menv.undef_lsymbol <- Sls.add ls menv.undef_lsymbol;
ls
let rec projty menv tvar ty : tty =
let rec projty menv tvar ty =
let rec aux ty =
match ty.ty_node with
| Tyvar tv -> Tyterm (t_var (Mtv.find tv tvar.tvar_term))
| Tyvar _ -> Tyterm ty
| Tyapp (ts,tyl) ->
try
Tyty (Mty.find ty menv.projty)
with Not_found ->
match menv.tenv with
| No_black_part ->
| Incomplete ->
(* In this configuration there is no term representing type,
all type are a type or are in the black part
(the or is not a xor)*)
......@@ -177,10 +149,10 @@ let rec projty menv tvar ty : tty =
(*Format.eprintf "projty : ts : %a env : %a@." Pretty.print_ts ts
print_env menv;*)
Tyty tty
| Tenv tenv ->
| Complete ->
let tyl = List.map aux tyl in
let tyl_red = List.map reduce_to_type tyl in
let ls =
let tys =
try
Mtyl.find tyl_red (Mts.find ts menv.defined_tsymbol)
with Not_found ->
......@@ -188,68 +160,116 @@ let rec projty menv tvar ty : tty =
with Not_found -> Mtyl.empty in
let args = List.fold_left (fun acc e ->
match e with
| Tyterm _ -> tenv.ty::acc
| Tyterm _ -> (create_tvsymbol (id_fresh "a"))::acc
| Tyty _ -> acc) [] tyl in
let ls = create_fsymbol (id_clone ts.ts_name) args tenv.ty in
let insts = Mtyl.add tyl_red ls insts in
let tys = if List.length args = List.length ts.ts_args
then ts
else create_tysymbol (id_clone ts.ts_name) args None in
let insts = Mtyl.add tyl_red tys insts in
menv.defined_tsymbol <-
Mts.add ts insts menv.defined_tsymbol;
menv.undef_lsymbol <- Sls.add ls menv.undef_lsymbol;
ls in
menv.undef_tsymbol <- Sts.add tys menv.undef_tsymbol;
tys in
let args = List.rev (List.fold_left (fun acc e ->
match e with
| Tyterm t -> t::acc
| Tyterm ty -> ty::acc
| Tyty _ -> acc) [] tyl) in
Tyterm (t_app ls args tenv.ty) in
let ty = ty_inst tvar.tvar_ty ty in
Tyterm (ty_app tys args) in
let ty = ty_inst tvar ty in
aux ty
let deco_res menv t ty =
match ty with
| Tyty _ -> t
| Tyterm tyterm ->
match menv.tenv with
| No_black_part -> assert false
| Tenv tenv -> t_app tenv.sort [tyterm;t] tenv.deco
let sort_app tenv ty t =
match tenv with
| No_black_part -> assert false
| Tenv tenv -> t_app tenv.sort [ty;t] tenv.deco
let projty_real menv tvar ty = reduce_to_real (projty menv tvar ty)
(* let reduce_to_default menv d = function *)
(* | Tyty ty -> ty *)
(* | Tyterm ty -> match menv.tenv with *)
(* | Incomplete -> ty *)
(* | Complete -> projty menv Mtv.empty d *)
let reduce_to_default menv tvar d ty =
match projty menv tvar ty with
| Tyty ty -> ty
| Tyterm _ -> ty_var d
let find_logic menv tvar p tyl ret =
if ls_equal p ps_equ then p else begin
let inst = ls_app_inst p tyl ret in
(*Format.eprintf "inst : %a@."
(Pp.print_iter2 Mtv.iter Pp.comma Pp.space Pp.nothing
Pretty.print_ty) inst;*)
let inst = Mtv.mapi (reduce_to_default menv tvar) inst in
let inst_l = Mtv.fold (fun _ v acc -> v::acc) inst [] in
(* Format.eprintf "p : %a | arg : %a| tyl = %a | inst_l : %i@." *)
(* Pretty.print_ls p *)
(* (Pp.print_list Pp.comma Pretty.print_ty) p.ls_args *)
(* (Pp.print_list Pp.comma Pretty.print_ty) *)
(* (List.map (fun t -> t.t_ty) tyl) *)
(* (List.length inst_l); *)
try
let insts = Mls.find p menv.defined_lsymbol in
Mtyl.find inst_l insts
with Not_found ->
let insts =
try
Mls.find p menv.defined_lsymbol
with Not_found ->
Mtyl.empty in
let proj ty = reduce_to_real (projty menv Mtv.empty ty) in
let arg = List.map (ty_inst inst) p.ls_args in
let arg = List.map proj arg in
let result = option_map (ty_inst inst) p.ls_value in
let result = option_map proj result in
let ls = if List.for_all2 ty_equal arg p.ls_args &&
option_eq ty_equal result p.ls_value
then p else create_lsymbol (id_clone p.ls_name) arg result in
let insts = Mtyl.add inst_l ls insts in
menv.defined_lsymbol <- Mls.add p insts menv.defined_lsymbol;
menv.undef_lsymbol <- Sls.add ls menv.undef_lsymbol;
(* Format.eprintf "fl : env : %a p : %a | inst : %a@." *)
(* print_env menv *)
(* Pretty.print_ls p *)
(* (Pp.print_list Pp.comma Pretty.print_ty) inst_l; *)
ls
end
(* let deco_res menv t ty = *)
(* match ty with *)
(* | Tyty _ -> t *)
(* | Tyterm tyterm -> *)
(* match menv.tenv with *)
(* | Incomplete -> assert false *)
(* | Tenv tenv -> t_app tenv.sort [tyterm;t] tenv.deco *)
(* let sort_app tenv ty t = *)
(* match tenv with *)
(* | Incomplete -> assert false *)
(* | Tenv tenv -> t_app tenv.sort [ty;t] tenv.deco *)
let conv_vs menv tvar vsvar vs =
let ty = projty menv tvar vs.vs_ty in
let vs'= create_vsymbol (id_clone vs.vs_name) (reduce_to_pos menv.tenv ty) in
(match ty with
| Tyterm t -> Mvs.add vs (sort_app menv.tenv t (t_var vs')) vsvar
| Tyty _ -> Mvs.add vs (t_var vs') vsvar),vs'
let conv_vs_let menv tvar vsvar vs =
let ty = projty menv tvar vs.vs_ty in
let vs'= create_vsymbol (id_clone vs.vs_name) (reduce_to_neg menv.tenv ty) in
(match ty with
| Tyterm _ -> Mvs.add vs (t_var vs') vsvar
| Tyty _ -> Mvs.add vs (t_var vs') vsvar),vs'
let ty = projty_real menv tvar vs.vs_ty in
let vs' = if ty_equal ty vs.vs_ty then vs else
create_vsymbol (id_clone vs.vs_name) ty in
Mvs.add vs (t_var vs') vsvar,vs'
(* The convertion of term and formula *)
let rec rewrite_term menv tvar vsvar t =
let fnT = rewrite_term menv tvar in
let fnF = rewrite_fmla menv tvar in
(* Format.eprintf "@[<hov 2>Term : %a =>@\n@?" Pretty.print_term t; *)
match t.t_node with
| Tconst _ -> t
| Tvar x -> Mvs.find x vsvar
| Tapp(p,tl) ->
let tl' = List.map (fnT vsvar) tl in
let tyl = List.map (fun t -> projty menv tvar t.t_ty) tl in
let ty = projty menv tvar t.t_ty in
let p = find_logic menv p tyl (Some ty) in
let app = t_app_infer p tl' in
deco_res menv app ty
let p = find_logic menv tvar p tl (Some t.t_ty) in
t_app p tl' (projty_real menv tvar t.t_ty)
| Tif(f, t1, t2) ->
t_if (fnF vsvar f) (fnT vsvar t1) (fnT vsvar t2)
| Tlet (t1, b) -> let u,t2,cb = t_open_bound_cb b in
let (vsvar',u) = conv_vs_let menv tvar vsvar u in
let (vsvar',u) = conv_vs menv tvar vsvar u in
let t1 = fnT vsvar t1 in let t2 = fnT vsvar' t2 in
t_let t1 (cb u t2)
| Tcase _ | Teps _ | Tbvar _ ->
......@@ -259,11 +279,11 @@ let rec rewrite_term menv tvar vsvar t =
and rewrite_fmla menv tvar vsvar f =
let fnT = rewrite_term menv tvar in
let fnF = rewrite_fmla menv tvar in
(* Format.eprintf "@[<hov 2>Fmla : %a =>@\n@?" Pretty.print_fmla f; *)
match f.f_node with
| Fapp(p, tl) ->
let tl' = List.map (fnT vsvar) tl in
let tyl = List.map (fun t -> projty menv tvar t.t_ty) tl in
let p = find_logic menv p tyl None in
let p = find_logic menv tvar p tl None in
f_app p tl'
| Fquant(q, b) ->
let vl, tl, f1, cb = f_open_quant_cb b in
......@@ -276,8 +296,10 @@ and rewrite_fmla menv tvar vsvar f =
let vl = List.rev vl in
f_quant q (cb vl tl f1)
| Flet (t1, b) -> let u,f2,cb = f_open_bound_cb b in
let (vsvar',u) = conv_vs_let menv tvar vsvar u in
let (vsvar',u) = conv_vs menv tvar vsvar u in
let t1 = fnT vsvar t1 and f2 = fnF vsvar' f2 in
(* Format.eprintf "u.vs_ty : %a == t1.t_ty : %a@." *)
(* Pretty.print_ty u.vs_ty Pretty.print_ty t1.t_ty; *)
assert (u.vs_ty == t1.t_ty);
f_let t1 (cb u f2)
| _ -> f_map (fnT vsvar) (fnF vsvar) f
......@@ -285,17 +307,15 @@ and rewrite_fmla menv tvar vsvar f =
(* Generation of all the possible instantiation of a formula *)
let gen_tvar env ts =
let aux tv tvarl =
let gen tvar ty = {tvar with tvar_ty = Mtv.add tv ty tvar.tvar_ty} in
let gen tvar ty = Mtv.add tv ty tvar in
let tvarl' = List.fold_left (fun acc tvar ->
Sty.fold (fun ty acc -> gen tvar ty :: acc) env.ekeep acc) [] tvarl in
match env.etenv with
| No_black_part -> tvarl'
| Tenv tenv ->
let gen acc tvar =
let vs = create_vsymbol (id_clone (tv.tv_name)) tenv.ty in
{tvar with tvar_term = Mtv.add tv vs tvar.tvar_term}::acc in
| Incomplete -> tvarl'
| Complete ->