Commit 036c6ce5 authored by Andrei Paskevich's avatar Andrei Paskevich

change default polymorphism encoding methods

in a series of tests on available examples, lightweight polymorphism
encoding techniques combined with a more agressive generation of
monomorphic instances (via Discriminate) show better results than
our earlier defaults.

In the same commit:
- remove Encoding_explicit (unsound), Encoding_decoexp (too naive),
  and Encoding_instantiate (subsumed by Discriminate)
- rename Encoding_decorate to Encoding_tags_full and Encoding_guard
  to Encoding_guards_full
- move Encoding_guards_full specific functions from Libencoding to
  Encoding_guards_full
- do not apply type protection in "encoding_tptp" and remove
  Protect_finite which is not needed anymore.
parent fdeda31a
...@@ -120,12 +120,10 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \ ...@@ -120,12 +120,10 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
LIB_TRANSFORM = simplify_formula inlining split_goal induction \ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
eliminate_definition eliminate_algebraic \ eliminate_definition eliminate_algebraic \
eliminate_inductive eliminate_let eliminate_if \ eliminate_inductive eliminate_let eliminate_if \
libencoding discriminate protect_finite \ libencoding discriminate encoding encoding_select \
encoding encoding_select \ encoding_guards_full encoding_tags_full \
encoding_decorate encoding_decoexp encoding_twin \ encoding_guards encoding_tags encoding_twin \
encoding_explicit encoding_guard encoding_sort \ encoding_sort simplify_array filter_trigger \
encoding_guards encoding_tags \
encoding_instantiate simplify_array filter_trigger \
introduction abstraction close_epsilon lift_epsilon \ introduction abstraction close_epsilon lift_epsilon \
eval_match instantiate_predicate smoke_detector eval_match instantiate_predicate smoke_detector
......
theory BuiltIn theory BuiltIn
meta "select_inst" "goal" meta "select_inst" "all"
meta "select_lskept" "none" meta "select_lskept" "all"
meta "select_lsinst" "goal" meta "select_lsinst" "none"
meta "select_kept" "none" meta "select_kept" "all"
end end
...@@ -9,6 +9,5 @@ unknown "No Proof Found" "" ...@@ -9,6 +9,5 @@ unknown "No Proof Found" ""
fail "Failure.*" "\"\\0\"" fail "Failure.*" "\"\\0\""
time "why3cpulimit time : %s s" time "why3cpulimit time : %s s"
import "tptp.gen" import "tptp.gen"
import "discrimination.gen"
...@@ -2,5 +2,5 @@ ...@@ -2,5 +2,5 @@
timeout "Time Out Virtual" timeout "Time Out Virtual"
import "tptp.gen" import "tptp.gen"
import "discrimination.gen"
...@@ -27,14 +27,19 @@ transformation "remove_triggers" ...@@ -27,14 +27,19 @@ transformation "remove_triggers"
trigger they can't appear since = can't appear *) trigger they can't appear since = can't appear *)
(*transformation "filter_trigger_builtin"*) (*transformation "filter_trigger_builtin"*)
transformation "encoding_tptp" (* this is sound as long as int is the only kept type *)
transformation "encoding_smt"
theory BuiltIn theory BuiltIn
syntax predicate (=) "(EQ %1 %2)" syntax predicate (=) "(EQ %1 %2)"
meta "enco_poly" "decorate"
meta "encoding : kept" type int meta "encoding : kept" type int
(* no symbol discrimination, no kept types *)
meta "select_inst" "none"
meta "select_lskept" "none"
meta "select_lsinst" "none"
meta "select_kept" "none"
end end
theory int.Int theory int.Int
......
...@@ -8,12 +8,5 @@ outofmemory "Out of Memory" ...@@ -8,12 +8,5 @@ outofmemory "Out of Memory"
unknown "No Proof Found" "" unknown "No Proof Found" ""
fail "Failure.*" "\"\\0\"" fail "Failure.*" "\"\\0\""
import "tptp.gen" import "tptp.gen"
import "discrimination.gen"
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
...@@ -24,8 +24,11 @@ transformation "eliminate_algebraic" ...@@ -24,8 +24,11 @@ transformation "eliminate_algebraic"
transformation "eliminate_if" transformation "eliminate_if"
transformation "eliminate_let" transformation "eliminate_let"
transformation "discriminate"
theory BuiltIn theory BuiltIn
syntax predicate (=) "equal(%1, %2)" syntax predicate (=) "equal(%1, %2)"
meta "eliminate_algebraic" "no_index" meta "eliminate_algebraic" "no_index"
end end
import "discrimination.gen"
...@@ -24,6 +24,7 @@ transformation "eliminate_algebraic" ...@@ -24,6 +24,7 @@ transformation "eliminate_algebraic"
transformation "eliminate_if" transformation "eliminate_if"
transformation "eliminate_let" transformation "eliminate_let"
transformation "discriminate"
transformation "encoding_tptp" transformation "encoding_tptp"
theory BuiltIn theory BuiltIn
......
...@@ -5,5 +5,5 @@ unknown "Time limit reached" "Time out" ...@@ -5,5 +5,5 @@ unknown "Time limit reached" "Time out"
unknown "Refutation not found" "" unknown "Refutation not found" ""
outofmemory "Memory limit exceeded" outofmemory "Memory limit exceeded"
import "tptp.gen" import "tptp.gen"
import "discrimination.gen"
...@@ -20,6 +20,7 @@ transformation "eliminate_algebraic" ...@@ -20,6 +20,7 @@ transformation "eliminate_algebraic"
transformation "eliminate_if" transformation "eliminate_if"
transformation "eliminate_let" transformation "eliminate_let"
transformation "discriminate"
transformation "encoding_tptp" transformation "encoding_tptp"
theory BuiltIn theory BuiltIn
...@@ -27,9 +28,4 @@ theory BuiltIn ...@@ -27,9 +28,4 @@ theory BuiltIn
meta "eliminate_algebraic" "no_index" meta "eliminate_algebraic" "no_index"
end end
(* import "discrimination.gen"
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
...@@ -212,7 +212,6 @@ let map env d = match d.d_node with ...@@ -212,7 +212,6 @@ let map env d = match d.d_node with
let task = Ssubst.fold conv_f substs [] in let task = Ssubst.fold conv_f substs [] in
task task
let ft_select_inst = let ft_select_inst =
((Hstr.create 17) : (Env.env,Sty.t) Trans.flag_trans) ((Hstr.create 17) : (Env.env,Sty.t) Trans.flag_trans)
...@@ -221,6 +220,7 @@ let ft_select_lskept = ...@@ -221,6 +220,7 @@ let ft_select_lskept =
let ft_select_lsinst = let ft_select_lsinst =
((Hstr.create 17) : (Env.env,Lsmap.t) Trans.flag_trans) ((Hstr.create 17) : (Env.env,Lsmap.t) Trans.flag_trans)
let metas_from_env env = 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_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 fold_ls _ insts s = Mtyl.fold fold_inst insts s in
......
...@@ -27,27 +27,25 @@ let meta_enco_kept = register_meta_excl "enco_kept" [MTstring] ...@@ -27,27 +27,25 @@ let meta_enco_kept = register_meta_excl "enco_kept" [MTstring]
~desc:"Specify@ the@ type@ protection@ transformation:@; \ ~desc:"Specify@ the@ type@ protection@ transformation:@; \
@[\ @[\
- @[<hov 2>twin: use@ conversion@ functions@ between@ the@ kept@ types@ \ - @[<hov 2>twin: use@ conversion@ functions@ between@ the@ kept@ types@ \
and@ the@ universal@ type@]@\n\ and@ the@ universal@ type@]@\
- @[<hov 2>instantiate: instantiate the axioms with the kept types@ \
and@ throw@ out@ polymorphic@ formulas@ (incomplete).@]@\n\
- @[<hov 2>instantiate_complete: same@ as@ 'instantiate'@ but@ keep@ \
polymorphic@ formulas.@]\
@]" @]"
let meta_enco_poly = register_meta_excl "enco_poly" [MTstring] let meta_enco_poly = register_meta_excl "enco_poly" [MTstring]
~desc:"Specify@ the@ type@ encoding@ transformation:@; \ ~desc:"Specify@ the@ type@ encoding@ transformation:@; \
@[\ @[\
- @[<hov 2>decorate: put@ type@ annotations@ on@ top@ of@ terms@]@\n\ - @[<hov 2>tags: protect@ variables@ in@ equalities@ \
- @[<hov 2>guard: add@ type@ conditions@ under@ quantifiers.@]\ with@ type@ annotations@]@\n\
- @[<hov 2>guards: protect@ variables@ in@ equalities@ \
with@ type@ conditions@]\n\
- @[<hov 2>tags_full: put@ type@ annotations@ on@ top@ \
of@ every@ term@]@\n\
- @[<hov 2>guards_full: add@ type@ conditions@ for@ every@ variable.@]\
@]" @]"
let def_enco_select_smt = "none" let def_enco_select_smt = "none"
let def_enco_kept_smt = "twin" let def_enco_kept_smt = "twin"
let def_enco_poly_smt = "decorate" let def_enco_poly_smt = "guards"
let def_enco_poly_tptp = "tags"
let def_enco_select_tptp = "none"
let def_enco_kept_tptp = "twin"
let def_enco_poly_tptp = "decorate"
let ft_select_kept = ((Hstr.create 17) : (Env.env,Sty.t) Trans.flag_trans) let ft_select_kept = ((Hstr.create 17) : (Env.env,Sty.t) Trans.flag_trans)
let ft_enco_kept = ((Hstr.create 17) : (Env.env,task) Trans.flag_trans) let ft_enco_kept = ((Hstr.create 17) : (Env.env,task) Trans.flag_trans)
...@@ -62,6 +60,11 @@ let select_kept def env = ...@@ -62,6 +60,11 @@ let select_kept def env =
in in
Trans.store trans Trans.store trans
let forget_kept = Trans.fold (fun hd task ->
match hd.task_decl.td_node with
| Meta (m,_) when meta_equal m Libencoding.meta_kept -> task
| _ -> add_tdecl task hd.task_decl) None
let encoding_smt env = Trans.seq [ let encoding_smt env = Trans.seq [
Libencoding.monomorphise_goal; Libencoding.monomorphise_goal;
select_kept def_enco_select_smt env; select_kept def_enco_select_smt env;
...@@ -71,11 +74,8 @@ let encoding_smt env = Trans.seq [ ...@@ -71,11 +74,8 @@ let encoding_smt env = Trans.seq [
let encoding_tptp env = Trans.seq [ let encoding_tptp env = Trans.seq [
Libencoding.monomorphise_goal; Libencoding.monomorphise_goal;
select_kept def_enco_select_tptp env; forget_kept;
Trans.print_meta Libencoding.debug Libencoding.meta_kept; Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_tptp env]
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;
Protect_finite.protect_finite]
let () = register_env_transform "encoding_smt" encoding_smt let () = register_env_transform "encoding_smt" encoding_smt
~desc:"Encode@ polymorphic@ types@ for@ provers@ with@ sorts." ~desc:"Encode@ polymorphic@ types@ for@ provers@ with@ sorts."
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
open Stdlib
open Ident
open Ty
open Term
open Decl
open Libencoding
(* 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 decorate tvar t =
let tty = term_of_ty tvar (t_type t) in
t_app ls_poly_deco [tty;t] t.t_ty
let findL = Wls.memoize 63 (fun ls ->
if ls_equal ls ps_equ then ls else
let tys = ls_ty_freevars ls in
if Stv.is_empty tys then ls else
let args = Stv.fold (fun _ l -> ty_type::l) tys ls.ls_args in
Term.create_lsymbol (id_clone ls.ls_name) args ls.ls_value)
let deco_term kept tvar =
let rec deco t = match t.t_node with
| Tvar v ->
if is_protected_vs kept v
then t else decorate tvar t
| Tapp (ls,_) when ls.ls_value <> None && not (is_protected_ls kept ls) ->
decorate tvar (expl t)
| Tconst _ ->
if Sty.mem (t_type t) kept
then t else decorate tvar t
| Teps tb ->
let v,f,close = t_open_bound_cb tb in
let t = t_eps (close v (deco f)) in
if is_protected_vs kept v
then t else decorate tvar t
| _ -> expl t
and expl t = match t.t_node with
| Tlet (t1,tb) ->
let v,e,close = t_open_bound_cb tb in
t_let (expl t1) (close v (deco e))
| Tapp (ls,tl) when not (ls_equal ls ps_equ) ->
let inst = ls_app_inst ls tl t.t_ty in
let add _ ty acc = term_of_ty tvar ty :: acc in
let tl = Mtv.fold add inst (List.map deco tl) in
t_app (findL ls) tl t.t_ty
| _ -> t_map deco t
in
deco
let ls_inf_type = create_psymbol (id_fresh "infinite") [ty_type]
let deco_decl kept inf_ts ma_map d = match d.d_node with
| Dtype { ts_def = Some _ } -> []
| Dtype ts when Mts.mem ts inf_ts ->
let ls = ls_of_ts ts in
let vs_of_tv v = create_vsymbol (id_clone v.tv_name) ty_type in
let vl = List.map vs_of_tv ts.ts_args in
let t = fs_app ls (List.map t_var vl) ty_type in
let inf_ts =
let id = id_fresh ("Inf_ts_" ^ ts.ts_name.id_string) in
let f = t_forall_close vl [] (ps_app ls_inf_type [t]) in
create_prop_decl Paxiom (create_prsymbol id) f in
let sort_id =
let id = id_fresh ("Sort_id_" ^ ts.ts_name.id_string) in
let ty_arg = ty_var (create_tvsymbol (id_fresh "a")) in
let vs_arg = create_vsymbol (id_fresh "x") ty_arg in
let t_arg = t_var vs_arg in
let t = fs_app ls_poly_deco [t; t_arg] ty_arg in
let f = t_forall_close (vs_arg::vl) [] (t_equ t t_arg) in
create_prop_decl Paxiom (create_prsymbol id) f in
[d; lsdecl_of_ts ts; inf_ts; sort_id]
| Dtype ts ->
let ls = ls_of_ts ts in
let vs_of_tv v = create_vsymbol (id_clone v.tv_name) ty_type in
let vl = List.map vs_of_tv ts.ts_args in
let t = fs_app ls (List.map t_var vl) ty_type in
let add mat v l = if not mat then l else
let id = id_fresh ("Inf_ts_" ^ ts.ts_name.id_string) in
let f = ps_app ls_inf_type [t] in
let h = ps_app ls_inf_type [t_var v] in
let f = t_forall_close vl [] (t_implies h f) in
create_prop_decl Paxiom (create_prsymbol id) f :: l in
let inf_tss =
try List.fold_right2 add (Mts.find ts ma_map) vl []
with Not_found -> [] in
[d; lsdecl_of_ts ts] @ inf_tss
| Ddata _ -> Printer.unsupportedDecl d
"Algebraic and recursively-defined types are \
not supported, run eliminate_algebraic"
| Dparam ls ->
[create_param_decl (findL ls)]
| Dlogic [ls,ld] when not (Sid.mem ls.ls_name d.d_syms) ->
let f = t_type_close (deco_term kept) (ls_defn_axiom ld) in
defn_or_axiom (findL 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"
| Dprop (k,pr,f) ->
[create_prop_decl k pr (t_type_close (deco_term kept) f)]
let d_infinite =
let pr = create_prsymbol (id_fresh "Infinite_type") in
let ty_arg = ty_var (create_tvsymbol (id_fresh "a")) in
let vs_ty = create_vsymbol (id_fresh "t") ty_type in
let vs_arg = create_vsymbol (id_fresh "x") ty_arg in
let t_ty = t_var vs_ty and t_arg = t_var vs_arg in
let t = fs_app ls_poly_deco [t_ty; t_arg] ty_arg in
let f = t_implies (ps_app ls_inf_type [t_ty]) (t_equ t t_arg) in
create_prop_decl Paxiom pr (t_forall_close [vs_ty;vs_arg] [] f)
let deco_init =
let init = Task.add_decl None d_ts_type in
let init = Task.add_param_decl init ls_poly_deco in
let init = Task.add_param_decl init ls_inf_type in
let init = Task.add_param_decl init ps_equ in
let init = Task.add_decl init d_infinite in
init
let deco kept =
Trans.on_tagged_ts Eliminate_algebraic.meta_infinite (fun infts ->
Trans.on_meta Eliminate_algebraic.meta_material (fun matl ->
let ma_map = Eliminate_algebraic.get_material_args matl in
Trans.decl (deco_decl kept infts ma_map) deco_init))
(** Monomorphisation *)
let ls_deco = create_fsymbol (id_fresh "sort") [ty_type;ty_base] ty_base
(* monomorphise a logical symbol *)
let lsmap kept = Wls.memoize 63 (fun ls ->
if ls_equal ls ls_poly_deco then ls_deco else
let prot_arg = is_protecting_id ls.ls_name in
let prot_val = is_protected_id ls.ls_name in
let neg ty = if prot_arg && Sty.mem ty kept then ty else ty_base in
let pos ty = if prot_val && Sty.mem ty kept then ty else ty_base in
let tyl = List.map neg ls.ls_args in
let tyr = Opt.map pos ls.ls_value in
if Opt.equal 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 mono_init = Task.add_decl None d_ts_base
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 Libencoding.meta_kept (fun kept ->
Trans.compose (deco kept) (mono kept))
let () = Hstr.replace Encoding.ft_enco_poly "decoexp" (Util.const t)
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(** transformation from polymorphic logic to untyped logic. The polymorphic
logic must not have finite support types. *)
(* dead code
open Ident
open Ty
open Term
open Libencoding
(** module with printing functions *)
module Debug = struct
let print_mtv vprinter fmter m =
Mtv.iter (fun key value -> Format.fprintf fmter "@[%a@] -> @[%a@]@."
Pretty.print_tv key vprinter value) m
(** utility to print a list of items *)
let rec print_list printer fmter = function
| [] -> Format.fprintf fmter ""
| e::es ->
if es = [] then
Format.fprintf fmter "@[%a@] %a" printer e (print_list printer) es
else
Format.fprintf fmter "@[%a@], %a" printer e (print_list printer) es
let debug x = Format.eprintf "%s@." x
end
(** {2 module to separate utilities from important functions} *)
module Transform = struct
(** creates a new logic symbol, with a different type if the
given symbol was polymorphic *)
let findL = Wls.memoize 63 (fun lsymbol ->
if ls_equal lsymbol ps_equ then lsymbol else
let new_ty = ls_ty_freevars lsymbol in
(* as many t as type vars *)
if Stv.is_empty new_ty then lsymbol (* same type *) else
let add _ acc = ty_type :: acc in
let args = Stv.fold add new_ty lsymbol.ls_args in
(* creates a new lsymbol with the same name but a different type *)
Term.create_lsymbol (id_clone lsymbol.ls_name) args lsymbol.ls_value)
(** {1 transformations} *)
(** translation of terms *)
let rec term_transform varM t = match t.t_node with
(* first case : predicate (not =), we must translate it and its args *)
| Tapp(f, terms) when not (ls_equal f ps_equ) ->
let terms = args_transform varM f terms t.t_ty in
t_app (findL f) terms t.t_ty
| _ -> (* default case : traverse *)
t_map (term_transform varM) t
and args_transform varM ls args ty =
(* Debug.print_list Pretty.print_ty Format.std_formatter type_vars; *)
let tv_to_ty = ls_app_inst ls args ty in
(* Debug.print_mtv Pretty.print_ty Format.err_formatter tv_to_ty; *)
let args = List.map (term_transform varM) args in
(* fresh args to be added at the beginning of the list of arguments *)
let add _ ty acc = term_of_ty varM ty :: acc in
Mtv.fold add tv_to_ty args
let param_transform ls = [Decl.create_param_decl (findL ls)]
(** transforms a list of logic declarations into another.
Declares new lsymbols with explicit polymorphic signatures. *)
let logic_transform decls =
(* if there is a definition, we must take it into account *)
let helper (lsymbol, ldef) =
let new_lsymbol = findL lsymbol in (* new lsymbol *)
let vars,expr,close = open_ls_defn_cb ldef in
let add v (vl,vm) =
let vs = Term.create_vsymbol (id_fresh "t") ty_type in
vs :: vl, Mtv.add v (t_var vs) vm
in
let vars,varM = Stv.fold add (ls_ty_freevars lsymbol) (vars,Mtv.empty) in
let t = term_transform varM expr in
close new_lsymbol vars t
in
[Decl.create_logic_decl (List.map helper decls)]
(** transform an inductive declaration *)
let ind_transform s idl =
let iconv (pr,f) = pr, Libencoding.t_type_close term_transform f in
let conv (ls,il) = findL ls, List.map iconv il in
[Decl.create_ind_decl s (List.map conv idl)]
(** transforms a proposition into another (mostly a substitution) *)
let prop_transform (prop_kind, prop_name, f) =
let quantified_fmla = Libencoding.t_type_close term_transform f in
[Decl.create_prop_decl prop_kind prop_name quantified_fmla]
end
(** {2 main part} *)
let decl d = match d.d_node with
| Dtype { ts_def = Some _ } -> []
| Dtype ts -> [d; Libencoding.lsdecl_of_ts ts]
| Ddata _ -> Printer.unsupportedDecl d
"Algebraic and recursively-defined types are \
not supported, run eliminate_algebraic"
| Dparam ls -> Transform.param_transform ls
| Dlogic ldl -> Transform.logic_transform ldl
| Dind (s, idl) -> Transform.ind_transform s idl
| Dprop prop -> Transform.prop_transform prop
let explicit = Trans.decl decl (Task.add_decl None d_ts_type)
(** {2 monomorphise task } *)
open Libencoding
let lsmap kept = Wls.memoize 63 (fun ls ->
let prot_arg = is_protecting_id ls.ls_name in
let prot_val = is_protected_id ls.ls_name in
let neg ty = if prot_arg && Sty.mem ty kept then ty else ty_base in
let pos ty = if prot_val && Sty.mem ty kept then ty else ty_base in
let ty_arg = List.map neg ls.ls_args in
let ty_res = Opt.map pos ls.ls_value in
if Opt.equal ty_equal ty_res ls.ls_value &&
List.for_all2 ty_equal ty_arg ls.ls_args then ls
else create_lsymbol (id_clone ls.ls_name) ty_arg ty_res)
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))
*)
(* This encoding method is unsound in presence of finite types. *)
(*
let () = Hstr.replace Encoding.ft_enco_poly "explicit"
(fun _ -> Trans.compose explicit monomorph)
*)
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
...@@ -9,9 +9,7 @@ ...@@ -9,9 +9,7 @@
(* *) (* *)
(********************************************************************) (********************************************************************)
(** transformation from polymorphic logic to untyped logic. The polymorphic (** transformation from polymorphic logic to many-sorted logic *)
logic must not have finite support types. *)
open Stdlib open Stdlib
open Ident open Ident
...@@ -40,6 +38,59 @@ end ...@@ -40,6 +38,59 @@ end
(** {2 module to separate utilities from important functions} *) (** {2 module to separate utilities from important functions} *)
module Lib = struct
(* function symbol selecting ty_type from ty_type^n *)
let ls_selects_of_ts = Wts.memoize 63 (fun ts ->
let create_select _ =
let preid = id_fresh ("select_"^ts.ts_name.id_string) in
create_fsymbol preid [ty_type] ty_type in
List.rev_map create_select ts.ts_args)
let ls_int_of_ty = create_fsymbol (id_fresh "int_of_ty") [ty_type] ty_int
(** definition of the previous selecting functions *)
let ls_selects_def_of_ts acc ts =
let ls = ls_of_ts ts in
let vars = List.rev_map
(fun _ -> create_vsymbol (id_fresh "x") ty_type) ts.ts_args
in
let tvars = List.map t_var vars in
(** type to int *)
let id = id_hash ts.ts_name in
let acc =
let t = fs_app ls tvars ty_type in
let f = t_equ (fs_app ls_int_of_ty [t] ty_int) (t_nat_const id) in
let f = t_forall_close vars [[t]] f in
let prsymbol = create_prsymbol (id_clone ts.ts_name) in
create_prop_decl Paxiom prsymbol f :: acc
in
(** select *)
let ls_selects = ls_selects_of_ts ts in
let fmlas = List.rev_map2
(fun ls_select value ->
let t = fs_app ls tvars ty_type in
let t = fs_app ls_select [t] ty_type in
let f = t_equ t value in
let f = t_forall_close vars [[t]] f in
f)
ls_selects tvars in
let create_props ls_select fmla =
let prsymbol = create_prsymbol (id_clone ls_select.ls_name) in
create_prop_decl Paxiom prsymbol fmla in
let props =
List.fold_left2 (fun acc x y -> create_props x y::acc)
acc ls_selects fmlas in
let add acc fs = create_param_decl fs :: acc in
List.fold_left add props ls_selects
(* convert a type declaration to a list of lsymbol declarations *)
let lsdecl_of_ts_select ts =
let defs = ls_selects_def_of_ts [] ts in
create_param_decl (ls_of_ts ts) :: defs
end
module Transform = struct module Transform = struct
(** type_of *) (** type_of *)
...@@ -57,7 +108,7 @@ module Transform = struct ...@@ -57,7 +108,7 @@ module Transform = struct
| Tyapp (ts,tyl) -> | Tyapp (ts,tyl) ->
let fold acc ls_select ty = let fold acc ls_select ty =
extract_tvar acc (fs_app ls_select [t] ty_type) ty in extract_tvar acc (fs_app ls_select [t] ty_type) ty in
List.fold_left2 fold acc (ls_selects_of_ts ts) tyl List.fold_left2 fold acc (Lib.ls_selects_of_ts ts) tyl
let type_close_select tvs ts fn f = let type_close_select tvs ts fn f =
let fold acc t = extract_tvar acc (app_type t) (t_type t) in let fold acc t = extract_tvar acc (app_type t) (t_type t) in
...@@ -142,7 +193,7 @@ module Transform = struct ...@@ -142,7 +193,7 @@ module Transform = struct
let add _ ty acc = term_of_ty varM ty :: acc in let add _ ty acc = term_of_ty varM ty :: acc in
Mtv.fold add tv_to_ty args Mtv.fold add tv_to_ty args
and f_type_close_select kept f' = let f_type_close_select kept f' =
let tvs = t_ty_freevars Stv.empty f' in let tvs = t_ty_freevars Stv.empty f' in
let trans fn acc f = match f.t_node with let trans fn acc f = match f.t_node with
| Tquant(Tforall as q,_) -> (* Exists same thing? *)