Commit 1814780c authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

remove Encoding_decorate_mono + some cleaning in Makefile

parent 02aa1780
......@@ -101,7 +101,10 @@ ifeq (@enable_local@,yes)
all: install_local
plugins: plugins.@OCAMLBEST@
.PHONY: byte opt clean depend all install install_local install_no_local
.PHONY: plugins plugins.byte plugins.opt
# Why library
......@@ -127,7 +130,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
eliminate_definition eliminate_algebraic \
eliminate_inductive eliminate_let eliminate_if \
encoding_distinction \
encoding_enumeration encoding encoding_decorate_mono \
encoding_enumeration encoding \
libencoding encoding_select \
encoding_decorate encoding_bridge \
encoding_explicit encoding_guard encoding_sort \
......@@ -460,7 +463,7 @@ byte: bin/why3ide.byte
opt: bin/why3ide.opt
bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@ -I @SQLITE3LIB@
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2 sqlite3
bin/why3ide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
......@@ -664,10 +667,10 @@ depend: .depend.tptp2why
rm -f src/tptp2why/*.cm[iox] src/tptp2why/*.o
rm -f src/tptp2why/*.cm* src/tptp2why/*.o
rm -f src/tptp2why/*.annot src/tptp2why/*.conflicts
rm -f src/tptp2why/*.output src/tptp2why/*.automaton
rm -f plugins/whytptp.cmxs plugins/whytptp.cmo
rm -f plugins/* plugins/whytptp.o
rm -f .depend.tptp2why
......@@ -751,7 +754,8 @@ install_local: bin/why3doc
.PHONY: bench test comp_bench_plugins
bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ $(TOOLS) $(DRIVERS) test-api
bench:: bin/why3.@OCAMLBEST@ bin/why3ml.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS)
$(MAKE) test-api
sh bench/bench \
"bin/why3.@OCAMLBEST@" \
(* *)
(* Copyright (C) 2010- *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* 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 *)
(* *)
(* This is a copy of encoding_decorate, it should be merged to it
when it is done *)
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 = register_meta "encoding_decorate : kept" [MTtysymbol]
(* From Encoding Polymorphism CADE07*)
type tenv = {rem_ls : Sls.t;
unsorted : ty;
sort : lsymbol;
real_to_int : lsymbol;
trans_lsymbol : lsymbol Hls.t;
trans_tsymbol : lsymbol Hts.t}
let load_prelude rem_ls env =
let prelude = Env.find_theory env why_filename "Prelude_mono" in
let sort = Theory.ns_find_ls prelude.th_export ["sort"] in
let int = Theory.ns_find_ls prelude.th_export ["int"] in
let real_to_int = Theory.ns_find_ls prelude.th_export ["real_to_int"] in
let task = None in
let task = Task.use_export task prelude in
let trans_tsymbol = Hts.create 17 in
Hts.add trans_tsymbol Ty.ts_int int;
{ rem_ls = rem_ls;
unsorted = ty_int;
sort = sort;
real_to_int = real_to_int;
trans_lsymbol = Hls.create 17;
trans_tsymbol = trans_tsymbol}
(* 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 ( (term_of_ty tenv tvar) l) tenv.unsorted
| 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.unsorted in
Htv.add tvar tv var;
let sort_app tenv tvar t ty =
let tty = term_of_ty tenv tvar ty in
t_app tenv.sort [tty;t] tenv.unsorted
(* Convert a type at the right of an arrow *)
let conv_ty_neg tenv _ty = tenv.unsorted
(* Convert a type at the left of an arrow *)
let conv_ty_pos tenv _ty = tenv.unsorted
(* Convert a logic symbols to the encoded one *)
let conv_ls tenv ls =
if ls_equal ls ps_equ
then ls
let tyl = (conv_ty_neg tenv) ls.ls_args in
let ty_res = Util.option_map (conv_ty_pos tenv) ls.ls_value in
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 = (fun _ -> tenv.unsorted) ts.ts_args in
create_fsymbol preid tyl tenv.unsorted
(* Convert the argument of a function from specials to deco or deco to
specials if needed*)
let conv_arg _tenv _tvar t _ty = t
(* Convert to undeco or to a specials an application *)
let conv_res_app tenv tvar p tl ty =
let tty = Util.of_option p.ls_value in
assert (ty_equal tty tenv.unsorted);
let t = t_app p tl tenv.unsorted in
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
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.unsorted, vsres in
(Mvs.add vs tres vsvar,vsres::acc)
let conv_vs_let tenv vsvar vs =
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
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 rec rewrite_term tenv tvar vsvar t =
(*Format.eprintf "@[<hov 2>Term : %a =>@\n@?" Pretty.print_term t;*)
let fnT = rewrite_term tenv tvar in
let fnF = rewrite_fmla tenv tvar vsvar in
match t.t_node with
| Tconst ConstInt _ -> sort_app tenv tvar t t.t_ty
| Tconst ConstReal _ ->
let t2 = t_app tenv.real_to_int [t] tenv.unsorted in
sort_app tenv tvar t2 t.t_ty
| Tvar x -> Mvs.find x vsvar
| Tapp(p,tl) ->
let tl = (fnT vsvar) tl in
let p = Hls.find tenv.trans_lsymbol p in
let tl = List.map2 (conv_arg tenv tvar) tl p.ls_args in
conv_res_app tenv tvar p tl 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 (vsvar',u) = conv_vs_let tenv vsvar u in
let t1 = fnT vsvar t1 in let t2 = fnT vsvar' t2 in
t_let t1 (close u t2)
| Tcase _ | Teps _ ->
Printer.unsupportedTerm t
"Encoding decorate : I can't encode this term"
and rewrite_fmla tenv tvar vsvar f =
(* Format.eprintf "@[<hov 2>Fmla : %a =>@\n@?" Pretty.print_fmla f;*)
let fnT = rewrite_term tenv tvar vsvar in
let fnF = rewrite_fmla tenv tvar in
match f.f_node with
| Fapp(p, tl) when ls_equal p ps_equ ->
let tl = fnT tl in
let ty = tenv.unsorted in
let tl = List.map2 (conv_arg tenv tvar) tl [ty;ty] in
f_app p tl
| Fapp(p, tl) ->
let tl = fnT tl in
let p = Hls.find tenv.trans_lsymbol p in
let tl = List.map2 (conv_arg tenv tvar) tl p.ls_args 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 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 (vsvar,u) = conv_vs_let tenv vsvar u in
let t1 = fnT t1 in let f2 = fnF vsvar f2 in
assert (u.vs_ty == t1.t_ty);
f_let t1 (close u f2)
| _ -> f_map fnT (fnF vsvar) f
let is_kept ls = List.for_all (fun ty -> ty_equal ty_int ty) ls.ls_args
&& option_apply true (ty_equal ty_int) ls.ls_value
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 ts_equal ts ts_int -> []
| Dtype [ts,Tabstract] ->
let tty =
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
[create_decl (create_logic_decl [(tty,None)])]
| Dtype _ -> Printer.unsupportedDecl
d "encoding_decorate : I can work only on abstract\
type which are not in recursive bloc."
| Dlogic l ->
let fn acc = function
| _ls, Some _ ->
d "encoding_decorate : I can't encode definition. \
Perhaps you could use eliminate_definition"
| ls1, None ->
let ls2 =
Hls.find tenv.trans_lsymbol ls1
with Not_found -> conv_ls tenv ls1 in
let acc = create_logic_decl [ls2,None] :: acc in
let acc = if Sls.mem ls1 tenv.rem_ls && is_kept ls1
then begin
let make _ = create_vsymbol (id_fresh "x") ty_int in
let vars = make ls1.ls_args in
let terms1 = t_var vars in
let tvar = Htv.create 0 in
let terms2 =
(fun t -> sort_app tenv tvar t ty_int) terms1 in
let fmla =
match ls1.ls_value with
| None ->
let f1 = f_app ls1 terms1 in
let f2 = f_app ls2 terms2 in
f_iff f1 f2
| Some _ ->
let t1 = t_app ls1 terms1 ty_int in
let t2 = t_app ls2 terms2 ty_int in
f_equ t1 t2 in
let fmla = f_forall_close vars [] fmla in
let name = create_prsymbol (id_clone ls1.ls_name) in
(create_prop_decl Paxiom name fmla)::d::acc
end else acc in
Hls.replace tenv.trans_lsymbol ls1 ls2;
acc in
List.rev_map create_decl (List.fold_left 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, fn l in *)
(* [create_ind_decl ( fn l)] *)
| Dprop (k,pr,f) ->
let tvar = Htv.create 17 in
let f = fnF tvar Mvs.empty f in
let tvl = Htv.fold (fun _ tv acc -> tv::acc) tvar [] in
let f = f_forall_close tvl [] 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)
let t env = Trans.on_tagged_ls Printer.meta_syntax_logic (fun rem_ls ->
let init_task,tenv = load_prelude rem_ls env in
Trans.tdecl (decl tenv) init_task)
let () = Trans.register_env_transform "encoding_decorate_mono" t
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