Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit cd251cd9 authored by Andrei Paskevich's avatar Andrei Paskevich

rewrite Encoding_decorate to use Libencoding

parent 7955d8e4
......@@ -21,265 +21,83 @@ open Util
open Ident
open Ty
open Term
open Task
open Theory
open Task
open Decl
open Encoding
let why_filename = ["transform" ; "encoding_decorate"]
open Libencoding
(* From Encoding Polymorphism CADE07*)
type tenv = {kept : Sts.t;
keptty : Sty.t;
deco : ty;
undeco : ty;
sort : lsymbol;
ty : ty;
trans_lsymbol : lsymbol Hls.t;
trans_tsymbol : lsymbol Hts.t;
trans_consts : lsymbol Hterm.t}
(* trans_lsymbol ne depend pour l'instant pas du but,
comme specials_type ne depend pas*)
let load_prelude kept env =
let prelude = Env.find_theory env why_filename "Prelude" in
let sort = Theory.ns_find_ls prelude.th_export ["sort"] in
let tyty = ty_app (Theory.ns_find_ts prelude.th_export ["ty"]) [] in
let deco = ty_app (Theory.ns_find_ts prelude.th_export ["deco"]) [] in
let undeco = ty_app (Theory.ns_find_ts prelude.th_export ["undeco"]) [] in
let task = None in
let task = Task.use_export task prelude in
let trans_tsymbol = Hts.create 17 in
let add ts sty = match ts.ts_def with
| Some ty -> Sty.add ty sty
| None -> Sty.add (ty_app ts []) sty in
let kepty = Sts.fold add kept Sty.empty in
let add_ts sts ts = Sts.add ts sts in
let add_ts ty sts = ty_s_fold add_ts sts ty in
let kept = Sty.fold add_ts kepty Sts.empty in
task,
{ kept = kept;
keptty = kepty;
deco = deco;
undeco = undeco;
ty = tyty;
sort = sort;
trans_lsymbol = Hls.create 17;
trans_tsymbol = trans_tsymbol;
trans_consts = Hterm.create 3;
}
(* Translate a type to a term *)
let rec term_of_ty tenv tvar ty =
match ty.ty_node with
| Tyapp (ts,l) ->
let tts = Hts.find tenv.trans_tsymbol ts in
t_app tts (List.map (term_of_ty tenv tvar) l) tenv.ty
| Tyvar tv ->
t_var (try Htv.find tvar tv
with Not_found ->
(let var = create_vsymbol
(id_fresh ("tv"^tv.tv_name.id_string))
tenv.ty in
Htv.add tvar tv var;
var))
let sort_app tenv tvar t ty =
let tty = term_of_ty tenv tvar ty in
t_app tenv.sort [tty;t] tenv.deco
(* Convert a type at the right of an arrow *)
let conv_ty_neg tenv ty =
if Sty.mem ty tenv.keptty then
ty
else
tenv.deco
(* Convert a type at the left of an arrow *)
let conv_ty_pos tenv ty =
if Sty.mem ty tenv.keptty then
ty
else
tenv.undeco
(* 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 (conv_ty_neg tenv) ls.ls_args in
let ty_res = Util.option_map (conv_ty_pos 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
let conv_ts tenv ts =
let preid = id_clone ts.ts_name in
let tyl = List.map (fun _ -> tenv.ty) ts.ts_args in
create_fsymbol preid tyl tenv.ty
(* Convert to undeco or to a specials an application *)
let conv_res_app tenv tvar t ty =
let tty = t.t_ty in
if Sty.mem tty tenv.keptty then t
else sort_app tenv tvar t ty
let conv_vs tenv tvar (vsvar,acc) vs =
let tres,vsres =
let ty_res = conv_ty_pos tenv vs.vs_ty in
if ty_equal ty_res vs.vs_ty then
t_var vs,vs
else
let tty = term_of_ty tenv tvar vs.vs_ty in
let vsres = (create_vsymbol (id_clone vs.vs_name) ty_res) in
let t = t_var vsres in
t_app tenv.sort [tty;t] tenv.deco, vsres in
(Mvs.add vs tres vsvar,vsres::acc)
let conv_vs_let vsvar vs ty_res =
let tres,vsres =
(* let ty_res = conv_ty_neg tenv vs.vs_ty in *)
if ty_equal ty_res vs.vs_ty then
t_var vs,vs
else
let vsres = (create_vsymbol (id_clone vs.vs_name) ty_res) in
let t = t_var vsres in
t, vsres in
(Mvs.add vs tres vsvar,vsres)
let conv_const tenv consts tvar t =
let fs =
try Hterm.find tenv.trans_consts t
with Not_found ->
let s = "const_"^Pp.string_of Pretty.print_term t in
let fs = create_fsymbol (id_fresh s) [] tenv.undeco in
Hterm.add tenv.trans_consts t fs; fs in
Hls.replace consts fs ();
conv_res_app tenv tvar (t_app fs [] tenv.undeco) t.t_ty
let rec rewrite_term tenv consts tvar vsvar t =
(* Format.eprintf "@[<hov 3>Term : %a : %a =>@\n@?" *)
(* Pretty.print_term t Pretty.print_ty t.t_ty; *)
let fnT = rewrite_term tenv consts tvar in
let fnF = rewrite_fmla tenv consts tvar vsvar in
match t.t_node with
| Tconst _ when Sty.mem t.t_ty tenv.keptty -> t
| Tconst _ -> conv_const tenv consts tvar t
| Tvar x -> Mvs.find x vsvar
| Tapp(p,tl) ->
let tl = List.map (fnT vsvar) tl in
let p = Hls.find tenv.trans_lsymbol p in
let t' = t_app_infer p tl in
conv_res_app tenv tvar t' t.t_ty
| Tif (f, t1, t2) ->
t_if (fnF f) (fnT vsvar t1) (fnT vsvar t2)
| Tlet (t1, b) ->
let u,t2,close = t_open_bound_cb b in
let t1 = fnT vsvar t1 in
let (vsvar,u) = conv_vs_let vsvar u t1.t_ty in
let t2 = fnT vsvar t2 in
t_let t1 (close u t2)
| Tcase _ | Teps _ | Tbvar _ ->
Printer.unsupportedTerm t
"Encoding decorate : I can't encode this term"
and rewrite_fmla tenv consts tvar vsvar f =
(* Format.eprintf "@[<hov>Fmla : %a =>@]@." Pretty.print_fmla f; *)
let fnT = rewrite_term tenv consts tvar vsvar in
let fnF = rewrite_fmla tenv consts tvar in
match f.f_node with
| Fapp(p, [a1;a2]) when ls_equal p ps_equ ->
let a1 = fnT a1 in let a2 = fnT a2 in
(* Format.eprintf "@[<hov>%a : %a = %a : %a@]@." *)
(* Pretty.print_term a1 Pretty.print_ty a1.t_ty *)
(* Pretty.print_term a2 Pretty.print_ty a2.t_ty; *)
f_equ a1 a2
| Fapp(p, tl) ->
let tl = List.map fnT tl in
let p = Hls.find tenv.trans_lsymbol p in
f_app p tl
| Fquant (q, b) ->
let vl, tl, f1, close = f_open_quant_cb b in
let (vsvar,vl) = List.fold_left (conv_vs tenv tvar) (vsvar,[]) vl in
let f1 = fnF vsvar f1 in
(* Ici un trigger qui ne match pas assez de variables
peut tre gnr *)
let tl = tr_map (rewrite_term tenv consts tvar vsvar) (fnF vsvar) tl in
let vl = List.rev vl in
f_quant q (close vl tl f1)
| Flet (t1, b) ->
let u,f2,close = f_open_bound_cb b in
let t1 = fnT t1 in
let (vsvar,u) = conv_vs_let vsvar u t1.t_ty in
let f2 = fnF vsvar f2 in
f_let t1 (close u f2)
| _ -> f_map fnT (fnF vsvar) 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_def = Some _},_] -> []
| Dtype [ts,Tabstract] ->
let tty =
try
Hts.find tenv.trans_tsymbol ts
with Not_found ->
let tty = conv_ts tenv ts in
Hts.add tenv.trans_tsymbol ts tty;
tty in
let td = [create_decl (create_logic_decl [(tty,None)])] in
if Sts.mem ts tenv.kept then (create_decl d)::td else td
| 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 tvar = Htv.create 17 in
let consts = Hls.create 3 in
let f = fnF consts tvar Mvs.empty f in
let tvl = Htv.fold (fun _ tv acc -> tv::acc) tvar [] in
let f = f_forall_close tvl [] f in
let add fs () acc = (create_decl (create_logic_decl [fs,None]))::acc in
Hls.fold add consts [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_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 s env in
Trans.tdecl (decl tenv) init_task)
(* polymorphic decoration function *)
let ls_poly_deco =
let tyvar = ty_var (create_tvsymbol (id_fresh "a")) in
create_fsymbol (id_fresh "sort") [ty_type;tyvar] tyvar
let rec deco_arg kept tvar t =
let t = deco_term kept tvar t in
if Sty.mem t.t_ty kept then t else
let tty = term_of_ty tvar t.t_ty in
t_app ls_poly_deco [tty;t] t.t_ty
and deco_term kept tvar t = match t.t_node with
| Tapp (fs,tl) -> t_app fs (List.map (deco_arg kept tvar) tl) t.t_ty
| _ -> t_map (deco_term kept tvar) (deco_fmla kept tvar) t
and deco_fmla kept tvar f = match f.f_node with
| Fapp (ps,tl) -> f_app ps (List.map (deco_arg kept tvar) tl)
| _ -> f_map (deco_term kept tvar) (deco_fmla kept tvar) f
let deco_decl kept d = match d.d_node with
| Dtype tdl ->
d :: lsdecl_of_tydecl tdl
| Dlogic ldl ->
let check = function
| _, Some _ -> Printer.unsupportedDecl d "eliminate definitions"
| _ -> ()
in
List.iter check ldl;
[d]
| Dind _ -> Printer.unsupportedDecl d "eliminate inductives"
| Dprop (k,pr,f) ->
let f = f_type_close (deco_fmla kept) f in
[create_prop_decl k pr f]
let d_poly_deco = create_logic_decl [ls_poly_deco, None]
let deco_init =
let init = Task.add_decl None d_ts_type in
let init = Task.add_decl init d_poly_deco in
init
let deco kept = Trans.decl (deco_decl kept) deco_init
(** Monomorphisation *)
let ts_deco = create_tysymbol (id_fresh "deco") [] None
let ty_deco = ty_app ts_deco []
let ls_deco = create_fsymbol (id_fresh "sort") [ty_type;ty_base] ty_deco
(* monomorphise a logical symbol *)
let lsmap kept = Wls.memoize 63 (fun ls ->
if ls_equal ls ls_poly_deco then ls_deco else
let neg ty = if Sty.mem ty kept then ty else ty_deco in
let pos ty = if Sty.mem ty kept then ty else ty_base in
let tyl = List.map neg ls.ls_args in
let tyr = Util.option_map pos ls.ls_value in
if Util.option_eq ty_equal tyr ls.ls_value
&& List.for_all2 ty_equal tyl ls.ls_args then ls
else create_lsymbol (id_clone ls.ls_name) tyl tyr)
let d_ts_deco = create_ty_decl [ts_deco, Tabstract]
let mono_init =
let init = Task.add_decl None d_ts_base in
let init = Task.add_decl init d_ts_deco in
init
let mono kept = Trans.decl (d_monomorph kept (lsmap kept)) mono_init
let t = Trans.on_meta Encoding.meta_kept (fun tds ->
let kept = Libencoding.get_kept_types tds in
Trans.compose (deco kept) (mono kept))
let () = Encoding.register_enco_poly "decorate" (const t)
let () = register_enco_poly "decorate" t
......@@ -17,9 +17,3 @@
(* *)
(**************************************************************************)
(** A transformation between polymorphic logic and multi-sorted logic*)
(** {{:http://www.lri.fr/~lescuyer/pdf/CADE-CL07.ps}
Handling Polymorphism in Automated Deduction}.
Jean-Francois Couchot et Stephane Lescuyer *)
val why_filename : string list
......@@ -114,28 +114,15 @@ module Transform = struct
in
[Decl.create_logic_decl (List.map helper decls)]
(** transforms a closed formula *)
let sentence_transform fmla =
let type_vars = f_ty_freevars Stv.empty fmla in
let varM = Stv.fold (* create a vsymbol for each type var *)
(fun x m -> Mtv.add x (create_vsymbol (id_fresh "t") ty_type) m)
type_vars Mtv.empty in
(* Debug.print_mtv Pretty.print_vs Format.err_formatter varM;
Format.eprintf "-----------@."; *)
(*universal quantification over ty vars*)
let new_fmla = fmla_transform varM fmla in
let vars = Mtv.fold (fun _ value acc -> value::acc) varM [] in
f_forall_close vars [] new_fmla
(** transform an inductive declaration *)
let ind_transform idl =
let iconv (pr,f) = pr, sentence_transform f in
let iconv (pr,f) = pr, Libencoding.f_type_close fmla_transform f in
let conv (ls,il) = findL ls, List.map iconv il in
[Decl.create_ind_decl (List.map conv idl)]
(** transforms a proposition into another (mostly a substitution) *)
let prop_transform (prop_kind, prop_name, fmla) =
let quantified_fmla = sentence_transform fmla in
let prop_transform (prop_kind, prop_name, f) =
let quantified_fmla = Libencoding.f_type_close fmla_transform f in
[Decl.create_prop_decl prop_kind prop_name quantified_fmla]
end
......
......@@ -126,8 +126,6 @@ let print_env fmt menv =
type tvar = ty Mtv.t
let why_filename = Encoding_decorate.why_filename
let rec projty menv tvar ty =
let rec aux ty =
match ty.ty_node with
......
......@@ -49,6 +49,14 @@ let rec term_of_ty tvmap ty = match ty.ty_node with
| Tyapp (ts,tl) ->
t_app (ls_of_ts ts) (List.map (term_of_ty tvmap) tl) ty_type
(* rewrite a closed formula modulo its free typevars *)
let f_type_close fn f =
let tvs = f_ty_freevars Stv.empty f in
let get_vs tv = create_vsymbol (id_clone tv.tv_name) ty_type in
let tvm = Stv.fold (fun v m -> Mtv.add v (get_vs v) m) tvs Mtv.empty in
let vl = Mtv.fold (fun _ vs acc -> vs::acc) tvm [] in
f_forall_close_simp vl [] (fn tvm f)
(* convert a type declaration to a list of lsymbol declarations *)
let lsdecl_of_tydecl tdl =
let add td acc = match td with
......
......@@ -39,6 +39,9 @@ val is_ls_of_ts : lsymbol -> bool
(* convert a type to a term of type ty_type *)
val term_of_ty : vsymbol Mtv.t -> ty -> term
(* rewrite a closed formula modulo its free typevars *)
val f_type_close : (vsymbol Mtv.t -> fmla -> fmla) -> fmla -> fmla
(* convert a type declaration to a list of lsymbol declarations *)
val lsdecl_of_tydecl : ty_decl list -> decl list
......
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