Skip to content

GitLab

why3
why3
Commit 5447cc14 authored by Francois Bobot's avatar Francois Bobot
Browse files
Options

corrige beaucoup d'erreur et d'incomprehension dans les encodages. 

bridge      + decorate : kept
instantiate + decorate : kept goal
parent 967d56ca
Hide whitespace changes
Inline Side-by-side
Showing with 160 additions and 90 deletions
src/transform/encoding_bridge.ml
View file @ 5447cc14
......@@ -35,8 +35,7 @@ type lconv = {tb2t : lsymbol;
t2tb : lsymbol;
tb : ty}
type tenv = {kept : Sts.t;
clone_builtin : tysymbol -> Theory.tdecl list;
type tenv = {kept : Sty.t;
specials : lconv Hty.t;
trans_lsymbol : lsymbol Hls.t;
trans_tsymbol : tysymbol Hts.t}
......@@ -44,60 +43,87 @@ type tenv = {kept : Sts.t;
comme specials_type ne depend pas*)
(* Translate a type to a type without kept *)
let rec ty_of_ty tenv ty =
match ty.ty_node with
| Tyapp (ts,[]) ->
let tts = try Hts.find tenv.trans_tsymbol ts
with Not_found -> ts in
ty_app tts []
| Tyapp (ts,l) -> ty_app ts (List.map (ty_of_ty tenv) l)
| Tyvar _ -> ty
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 type_tb = Theory.ns_find_ts builtin.th_export ["tb"] in
let logic_tb2t = Theory.ns_find_ls builtin.th_export ["tb2t"] in
let logic_t2tb = Theory.ns_find_ls builtin.th_export ["t2tb"] in
let trans_tsymbol = Hts.create 17 in
let clone_builtin ts =
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 tenv_tmp =
{ kept = Sty.empty;
specials = specials;
trans_lsymbol = Hls.create 17;
trans_tsymbol = trans_tsymbol} in
let clone_builtin ts (task,sty) =
let ty = match ts.ts_def with
| Some ty -> ty
| None -> try ty_app ts [] with BadTypeArity(_,_,_) ->
failwith "kept without definition must be constant" in
let add_ts task ts = add_ty_decl task [ts,Tabstract] in
let task = ty_s_fold add_ts task ty in
let is_constant =
match ty.ty_node with
| Tyapp (_,[]) -> true
| _ -> false in
let ts_head =
match ty.ty_node with
| Tyapp (ts,_) -> ts
| _ -> assert false in
let task = add_ts task ts in
let tb = create_tysymbol (id_clone ts_head.ts_name) []
(if is_constant then None else Some (ty_of_ty tenv_tmp ty)) in
let task = add_ts task tb in
let tytb = ty_app tb [] in
let tb2t = create_fsymbol (id_clone logic_t2tb.ls_name) [tytb] ty in
let t2tb = create_fsymbol (id_clone logic_t2tb.ls_name) [ty] tytb in
let task = add_logic_decl task [tb2t,None] in
let task = add_logic_decl task [t2tb,None] 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
~ts:[type_t,ts;type_tb,tb]
~ls:[logic_t2tb,t2tb;logic_tb2t,tb2t] ~lemma:[] ~goal:[] in
let task = Task.clone_export task builtin th_inst in
let lconv = { tb2t = tb2t; t2tb = t2tb; tb = ty_app tb []} in
let task = Task.use_export None 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}
(* Add the constant sort to trans_tsymbol *)
if is_constant then Hts.add trans_tsymbol ts_head tb;
Hty.add specials ty lconv;
task,Sty.add ty sty in
let task,kept = Sts.fold clone_builtin kept (task,Sty.empty) in
task, { tenv_tmp with kept = kept}
(* 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 =
let conv_ty tenv ty =
if Hty.mem tenv.specials ty then ty else ty_of_ty tenv ty
let is_kept tenv ts = ts.ts_args = [] && Sts.mem ts tenv.kept
(* let is_kept tenv ts = ts.ts_args = [] && Sty.mem ts tenv.kept *)
(* Convert a variable *)
let conv_vs tenv vs =
let ty = conv_ty tenv vs.vs_ty in
if ty_equal ty vs.vs_ty then vs else
create_vsymbol (id_dup vs.vs_name) ty
(* 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
let tyl = List.map (conv_ty tenv) ls.ls_args in
let ty_res = Util.option_map (conv_ty 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
......@@ -110,17 +136,12 @@ 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
(* polymorph specials t2tb *)
let tylconv = Hty.find tenv.specials tty in
t_app tylconv.t2tb [t] tylconv.tb
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
(* polymorph not specials *)
t
(* Convert with a bridge an application if needed *)
let conv_res_app tenv p tl tty =
......@@ -137,38 +158,68 @@ let conv_res_app tenv p tl tty =
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 rec rewrite_term tenv vsvar 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
let t = match t.t_node with
| Tvar vs -> Mvs.find vs vsvar
| Tapp(p,tl) ->
let tl = List.map fnT tl in
let tl = List.map (fnT vsvar) 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
| _ -> t_map fnT fnF t
| Tlet (t1, b) ->
let u,t2,close = t_open_bound_cb b in
let t1 = fnT vsvar t1 in
let u' = conv_vs tenv u in
let vsvar = Mvs.add u (t_var u') vsvar in
let t2 = fnT vsvar t2 in
t_let t1 (close u t2)
| _ -> t_map (fnT vsvar) (fnF vsvar) t in
(* Format.eprintf "@[<hov 2>Term : => %a : %a@\n@?" Pretty.print_term t *)
(* Pretty.print_ty t.t_ty; *)
t
and rewrite_fmla tenv f =
and rewrite_fmla tenv vsvar 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, [t1;t2]) when ls_equal p ps_equ ->
f_equ (fnT t1) (fnT t2)
f_equ (fnT vsvar t1) (fnT vsvar t2)
| Fapp(p, tl) ->
let tl = List.map fnT tl in
let tl = List.map (fnT vsvar) 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
| Fquant (q, b) ->
let vl, tl, f1, close = f_open_quant_cb b in
let conv_vs (vsvar,l) vs =
let vs' = conv_vs tenv vs in
Mvs.add vs (t_var vs') vsvar,vs'::l in
let (vsvar,vl) = List.fold_left conv_vs (vsvar,[]) vl in
let f1 = fnF vsvar f1 in
(* Ici un trigger qui ne match pas assez de variables
peut être généré *)
let tl = tr_map (fnT 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 vsvar t1 in
let u' = conv_vs tenv u in
let vsvar = Mvs.add u (t_var u') vsvar in
let f2 = fnF vsvar f2 in
f_let t1 (close u f2)
| _ -> f_map (fnT vsvar) (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,Tabstract] when is_kept tenv ts ->
tenv.clone_builtin ts
(* | 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 \
......@@ -194,7 +245,7 @@ let decl (tenv:tenv) d =
(* 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
let f = fnF Mvs.empty f in
[create_decl (create_prop_decl k pr f)]
(*
......
src/transform/encoding_decorate.ml
View file @ 5447cc14
......@@ -53,7 +53,14 @@ let load_prelude kept env =
let task = None in
let task = Task.use_export task prelude in
let trans_tsymbol = Hts.create 17 in
let kepty = Sts.fold (fun ts -> Sty.add (ty_app ts [])) kept Sty.empty 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 ty sts = match ty.ty_node with
| Tyapp (ts,[]) -> Sts.add ts sts
| _ -> sts in
let kept = Sty.fold add kepty Sts.empty in
task,
{ kept = kept;
keptty = kepty;
......@@ -223,6 +230,7 @@ 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] when is_kept tenv ts -> [create_decl d]
| Dtype [ts,Tabstract] ->
let tty =
......@@ -265,14 +273,13 @@ let decl (tenv:tenv) d =
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_task_tdecl)
res;
res
*)
(* 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
......
src/transform/encoding_instantiate.ml
View file @ 5447cc14
......@@ -189,23 +189,23 @@ let projty_real menv tvar ty = reduce_to_real (projty menv tvar ty)
let reduce_to_default menv tvar d ty =
match projty menv tvar ty with
| Tyty ty -> ty
| Tyty _ -> (*keep the term unfolded *) ty_inst tvar 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;*)
(* 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 *)
(* Format.eprintf "p : %a | arg : %a| tyl = %a | inst_l : %a@." *)
(* 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); *)
(* (Pp.print_list Pp.comma Pretty.print_ty) *)
(* (List.map (fun t -> (projty_real menv tvar t.t_ty)) tyl) *)
(* (Pp.print_list Pp.comma Pretty.print_ty) inst_l; *)
try
let insts = Mls.find p menv.defined_lsymbol in
Mtyl.find inst_l insts
......@@ -215,18 +215,22 @@ let find_logic menv tvar p tyl ret =
Mls.find p menv.defined_lsymbol
with Not_found ->
Mtyl.empty in
(* proj fold the types previously kept unfold in inst *)
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
(* Format.eprintf "arg : %a ; result : %a@." *)
(* (Pp.print_list Pp.comma Pretty.print_ty) arg *)
(* (Pp.print_option Pretty.print_ty) result; *)
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@." *)
(* 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; *)
......@@ -259,7 +263,7 @@ 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
let t = match t.t_node with
| Tconst _ -> t
| Tvar x -> Mvs.find x vsvar
| Tapp(p,tl) ->
......@@ -274,7 +278,10 @@ let rec rewrite_term menv tvar vsvar t =
t_let t1 (cb u t2)
| Tcase _ | Teps _ | Tbvar _ ->
Printer.unsupportedTerm t
"Encoding instantiate : I can't encode this term"
"Encoding instantiate : I can't encode this term" in
(* Format.eprintf "@[<hov 2>Term : => %a : %a@\n@?" *)
(* Pretty.print_term t Pretty.print_ty t.t_ty; *)
t
and rewrite_fmla menv tvar vsvar f =
let fnT = rewrite_term menv tvar in
......@@ -394,7 +401,7 @@ Perhaps you could use eliminate_definition"
undef_tsymbol = Sts.empty;
} in
let conv_f task tvar =
(* Format.eprintf "f0 : %a@. env : %a@." Pretty.print_fmla *)
(* Format.eprintf "f0 : %a@. env : %a@." Pretty.print_fmla *)
(* (f_ty_subst tvar Mvs.empty f) *)
(* print_env menv; *)
let f = rewrite_fmla menv tvar Mvs.empty f in
......@@ -439,11 +446,7 @@ let monomorphise_goal =
let collect_green_part tds =
(* int and real are always taken in the green part (the constants
can't be written otherwise). Trigger that only when Int or Real
theory is used should not be sufficient. *)
let sts = Sts.add ts_int (Sts.singleton ts_real) in
let sts = Task.find_tagged_ts meta_kept tds sts in
let sts = Task.find_tagged_ts meta_kept tds Sts.empty in
let extract ts tys =
assert (ts.ts_args = []); (* UnsupportedTySymbol? *)
Sty.add (match ts.ts_def with
......@@ -514,16 +517,21 @@ let () =
(* Select *)
let find_mono ~only_mono sty f =
let add sty ty = if is_ty_mono ~only_mono ty then Sty.add ty sty else sty in
let rec ty_add sty ty = ty_fold ty_add (Sty.add ty sty) ty in
let add sty ty = if is_ty_mono ~only_mono ty then
ty_add sty ty else sty in
f_fold_ty add sty f
let create_meta_ty ty acc =
let create_meta_ty ty =
let name = id_fresh "meta_ty" in
let ts = create_tysymbol name [] (Some ty) in
(create_meta meta_kept [MAts ts])::acc
(create_meta meta_kept [MAts ts])
(* Weak table is useless since ty is in ts *)
let create_meta_ty = Wty.memoize 17 create_meta_ty
let create_meta_tyl sty d =
Sty.fold create_meta_ty sty [create_decl d]
Sty.fold (flip $ cons create_meta_ty) sty [create_decl d]
let mono_in_goal pr f =
let sty = (try find_mono ~only_mono:true Sty.empty f
......
src/util/util.ml
View file @ 5447cc14
......@@ -25,6 +25,8 @@ let const f _ = f
let flip f x y = f y x
let cons f acc x = (f x)::acc
(* useful option combinators *)
let of_option = function None -> assert false | Some x -> x
......
src/util/util.mli
View file @ 5447cc14
......@@ -25,6 +25,8 @@ val const : 'a -> 'b -> 'a
val flip : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
val cons : ('a -> 'b) -> 'b list -> 'a -> 'b list
(* useful option combinators *)
val of_option : 'a option -> 'a
......
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