separate symbol discrimination from polymorphism encoding

Makefile.in

@@ -125,9 +125,8 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
 		inlining split_goal \
 		eliminate_definition eliminate_algebraic \
 		eliminate_inductive eliminate_let eliminate_if \
-		encoding_distinction \
-		encoding_enumeration encoding \
-		libencoding encoding_select \
+		encoding_enumeration encoding libencoding \
+		encoding_distinction encoding_select \
 		encoding_decorate encoding_bridge \
 		encoding_explicit encoding_guard encoding_sort \
 		encoding_instantiate simplify_array filter_trigger \

bench/encoding/create_bench.sh

@@ -2,13 +2,13 @@
 
 PROVER=$1
 SELECT_INST=Inst_$2
-SELECT_KEPT=Kept_$3
-SELECT_LSKEPT=Lskept_$4
-PRODUCT_MODE=Product_$5
+SELECT_LSKEPT=Lskept_$3
+SELECT_LSINST=Lsinst_$4
+SELECT_KEPT=Kept_$5
 ENCO_KEPT=Kept_$6
 ENCO_POLY=Poly_$7
 
-BENCH_NAME="${PROVER}_${SELECT_INST}_${SELECT_KEPT}_${SELECT_LSKEPT}_${PRODUCT_MODE}_${ENCO_KEPT}_${ENCO_POLY}"
+BENCH_NAME="${PROVER}_${SELECT_INST}_${SELECT_LSKEPT}_${SELECT_LSINST}_${SELECT_KEPT}_${ENCO_KEPT}_${ENCO_POLY}"
 
 FILE=${BENCH_NAME}.rc
 
@@ -17,9 +17,9 @@ sed template_rc \
     -e "s/@BENCH_NAME@/$BENCH_NAME/" \
     -e "s/@PROVER@/$PROVER/" \
     -e "s/@SELECT_INST@/$SELECT_INST/" \
-    -e "s/@SELECT_KEPT@/$SELECT_KEPT/" \
     -e "s/@SELECT_LSKEPT@/$SELECT_LSKEPT/" \
-    -e "s/@PRODUCT_MODE@/$PRODUCT_MODE/" \
+    -e "s/@SELECT_LSINST@/$SELECT_LSINST/" \
+    -e "s/@SELECT_KEPT@/$SELECT_KEPT/" \
     -e "s/@ENCO_KEPT@/$ENCO_KEPT/" \
     -e "s/@ENCO_POLY@/$ENCO_POLY/" \
     > $FILE
@@ -38,4 +38,4 @@ sed template_rc \
 #     *\) *)
 #         echo "Unknown error"; *)
 #         exit 2 *)
-# esac *)
\ No newline at end of file
+# esac *)

bench/encoding/gen_allbench.sh

 #!/bin/dash
 
 PROVER="z3 cvc3 yices"
-SELECT_INST="nothing goal context"
-SELECT_KEPT="nothing goal context"
-SELECT_LSKEPT="nothing goal context"
-PRODUCT_MODE="nothing only_kept some_kept"
+SELECT_INST="none goal all"
+SELECT_LSKEPT="none goal all"
+SELECT_LSINST="none goal all"
+SELECT_KEPT="none goal all"
 ENCO_KEPT="twin partial"
 ENCO_POLY="deco explicit guard"
 
@@ -12,10 +12,10 @@ dirname=$(dirname $0)
 
 for P in $PROVER; do
 for SI in $SELECT_INST; do
+for SLK in $SELECT_LSKEPT; do
+for SLI in $SELECT_LSINST; do
 for SK in $SELECT_KEPT; do
-for SL in $SELECT_LSKEPT; do
-for PM in $PRODUCT_MODE; do
 for EK in $ENCO_KEPT; do
 for EP in $ENCO_POLY; do
-$dirname/create_bench.sh $P $SI $SK $SL $PM $EK $EP
-done done done done done done done
\ No newline at end of file
+$dirname/create_bench.sh $P $SI $SLK $SLI $SK $EK $EP
+done done done done done done done

bench/encoding/meta.why

@@ -23,52 +23,52 @@ theory Poly_deco
   meta "enco_poly" "decorate"
 end
 
-theory Inst_nothing
-  meta "select_inst" "nothing"
+theory Inst_none
+  meta "select_inst" "none"
 end
 
 theory Inst_goal
   meta "select_inst" "goal"
 end
 
-theory Inst_context
+theory Inst_all
   meta "select_inst" "all"
 end
 
-theory Kept_nothing
-  meta "select_kept" "nothing"
+theory Lskept_none
+  meta "select_lskept" "none"
 end
 
-theory Kept_goal
-  meta "select_kept" "goal"
+theory Lskept_goal
+  meta "select_lskept" "goal"
 end
 
-theory Kept_context
-  meta "select_kept" "all"
+theory Lskept_all
+  meta "select_lskept" "all"
 end
 
-theory Lskept_nothing
-  meta "select_lskept" "nothing"
+theory Lsinst_none
+  meta "select_lsinst" "none"
 end
 
-theory Lskept_goal
-  meta "select_lskept" "goal"
+theory Lsinst_goal
+  meta "select_lsinst" "goal"
 end
 
-theory Lskept_context
-  meta "select_lskept" "all"
+theory Lsinst_all
+  meta "select_lsinst" "all"
 end
 
-theory Product_nothing
-  meta "completion_mode" "nothing"
+theory Kept_none
+  meta "select_kept" "none"
 end
 
-theory Product_only_kept
-  meta "completion_mode" "only_kept"
+theory Kept_goal
+  meta "select_kept" "goal"
 end
 
-theory Product_some_kept
-  meta "completion_mode" "some_kept"
+theory Kept_all
+  meta "select_kept" "all"
 end
 
 theory KeptIntReal
@@ -76,4 +76,4 @@ theory KeptIntReal
   use real.Real
   meta "encoding : kept" type Int.int
   meta "encoding : kept" type Real.real
-end
\ No newline at end of file
+end

bench/encoding/template_rc

@@ -2,9 +2,9 @@
 prover = "@PROVER@"
 loadpath = "."
 use = "meta.@SELECT_INST@"
-use = "meta.@SELECT_KEPT@"
 use = "meta.@SELECT_LSKEPT@"
-use = "meta.@PRODUCT_MODE@"
+use = "meta.@SELECT_LSINST@"
+use = "meta.@SELECT_KEPT@"
 use = "meta.@ENCO_KEPT@"
 use = "meta.@ENCO_POLY@"
 

drivers/alt_ergo.drv

@@ -13,7 +13,7 @@ time "Valid (%s)"
 time "why3cpulimit time : %s s"
 
 (* À discuter *)
-transformation "simplify_recursive_definition"
+(*transformation "simplify_recursive_definition"*)
 transformation "inline_trivial"
 
 transformation "eliminate_builtin"

drivers/alt_ergo_smt2.drv

@@ -9,7 +9,7 @@ valid "^unsat"
 unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
 time "why3cpulimit time : %s s"
 
-transformation "simplify_recursive_definition"
+(*transformation "simplify_recursive_definition"*)
 transformation "inline_trivial"
 
 transformation "eliminate_builtin"

drivers/coq.drv

@@ -11,7 +11,7 @@ prelude "(* This file is generated by Why3's Coq driver *)"
 prelude "(* Beware! Only edit allowed sections below    *)"
 
 (* À discuter *)
-transformation "simplify_recursive_definition"
+(*transformation "simplify_recursive_definition"*)
 transformation "inline_trivial"
 
 transformation "eliminate_builtin"

drivers/cvc3_bare.drv

@@ -10,7 +10,7 @@ unknown "Unknown." ""
 time "why3cpulimit time : %s s"
 
 (* À discuter *)
-transformation "simplify_recursive_definition"
+(*transformation "simplify_recursive_definition"*)
 transformation "inline_trivial"
 
 transformation "eliminate_builtin"
@@ -21,6 +21,7 @@ transformation "eliminate_algebraic_smt"
 transformation "simplify_formula"
 (*transformation "simplify_trivial_quantification"*)
 
+transformation "discriminate"
 transformation "encoding_smt"
 
 theory BuiltIn

drivers/discrimination.gen

 theory BuiltIn
   meta "select_inst" "goal"
-  meta "select_kept" "goal"
-  meta "select_lskept" "nothing"
-  meta "completion_mode" "only_kept"
+  meta "select_lskept" "none"
+  meta "select_lsinst" "goal"
+  meta "select_kept" "none"
 end
 

drivers/gappa.drv

@@ -11,7 +11,7 @@ unknown "no contradiction was found\\|some enclosures were not satisfied" "Unkno
 time "why3cpulimit time : %s s"
 fail "Error: \\(.*\\)" "\\1"
 
-transformation "simplify_recursive_definition"
+(*transformation "simplify_recursive_definition"*)
 transformation "inline_trivial"
 transformation "eliminate_builtin"
 transformation "inline_all"

drivers/simplify.drv

@@ -9,7 +9,7 @@ valid "\\bValid\\b"
 unknown "\\bInvalid\\b" "Unknown"
 time "why3cpulimit time : %s s"
 
-transformation "simplify_recursive_definition"
+(*transformation "simplify_recursive_definition"*)
 transformation "inline_trivial"
 
 transformation "eliminate_builtin"

drivers/tptp.drv

@@ -18,7 +18,7 @@ time "why3cpulimit time : %s s"
 
 (* to be improved *)
 
-transformation "simplify_recursive_definition"
+(*transformation "simplify_recursive_definition"*)
 transformation "inline_trivial"
 
 transformation "eliminate_builtin"

drivers/vampire.drv

@@ -18,7 +18,7 @@ time "why3cpulimit time : %s s"
 
 (* to be improved *)
 
-transformation "simplify_recursive_definition"
+(*transformation "simplify_recursive_definition"*)
 transformation "inline_trivial"
 
 transformation "eliminate_builtin"

drivers/verit.drv

@@ -10,7 +10,7 @@ unknown "^\\(unknown\\|sat\\)" "Unknown"
 time "why3cpulimit time : %s s"
 
 (* À discuter *)
-transformation "simplify_recursive_definition"
+(*transformation "simplify_recursive_definition"*)
 transformation "inline_trivial"
 
 transformation "eliminate_builtin"

drivers/yices_bare.drv

@@ -10,7 +10,7 @@ unknown "\\bunknown\\b\\|\\bsat\\b\\|feature not supported: non linear problem"
 time "why3cpulimit time : %s s"
 
 (* À discuter *)
-transformation "simplify_recursive_definition"
+(*transformation "simplify_recursive_definition"*)
 transformation "inline_trivial"
 
 transformation "eliminate_builtin"
@@ -21,6 +21,7 @@ transformation "eliminate_algebraic_smt"
 transformation "simplify_formula"
 (*transformation "simplify_trivial_quantification"*)
 
+transformation "discriminate"
 transformation "encoding_smt"
 transformation "encoding_sort"
 

drivers/z3_bare.drv

@@ -12,7 +12,7 @@ time "why3cpulimit time : %s s"
 
 
 (* À discuter *)
-transformation "simplify_recursive_definition"
+(*transformation "simplify_recursive_definition"*)
 transformation "inline_trivial"
 
 transformation "eliminate_builtin"
@@ -22,6 +22,8 @@ transformation "eliminate_algebraic_smt"
 
 transformation "simplify_formula"
 (*transformation "simplify_trivial_quantification"*)
+
+transformation "discriminate"
 transformation "encoding_smt"
 
 theory BuiltIn

drivers/z3_smtv1.drv

@@ -11,7 +11,7 @@ time "why3cpulimit time : %s s"
 
 
 (* À discuter *)
-transformation "simplify_recursive_definition"
+(*transformation "simplify_recursive_definition"*)
 transformation "inline_trivial"
 
 transformation "eliminate_builtin"

src/core/trans.ml

@@ -38,7 +38,6 @@ let identity   x =  x
 let identity_l x = [x]
 
 let return x = fun _ -> x
-let bind f g task = g (f task) task
 
 let conv_res c f x = c (f x)
 
@@ -57,6 +56,8 @@ end)
 
 let store fn = Wtask.memoize_option 63 fn
 
+let bind f g = store (fun task -> g (f task) task)
+
 let fold fn v =
   let h = Wtask.create 63 in
   let rewind acc task =
@@ -85,9 +86,8 @@ let fold fn v =
 let fold_l fn v = fold (fun task -> list_apply (fn task)) [v]
 
 let fold_map   fn v t = conv_res snd            (fold   fn (v, t))
-(* We keep the order is important for the user. So we use
-   List.map is instead of List.map_rev *)
 let fold_map_l fn v t = conv_res (List.map snd) (fold_l fn (v, t))
+(* we use List.map instead of List.map_rev to preserve the order *)
 
 let gen_decl add fn =
   let fn = Wdecl.memoize 63 fn in
@@ -136,7 +136,7 @@ let rewriteTF fnT fnF = rewrite (TermTF.t_select fnT fnF)
 
 let gen_add_decl add decls = function
   | Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
-    add_decl (List.fold_left add prev decls) d
+      add_decl (List.fold_left add prev decls) d
   | _ -> assert false
 
 let add_decls  = gen_add_decl add_decl

src/core/trans.mli

@@ -49,14 +49,11 @@ val seq_l : task tlist list -> task tlist
 val fold   : (task_hd -> 'a -> 'a     ) -> 'a -> 'a trans
 val fold_l : (task_hd -> 'a -> 'a list) -> 'a -> 'a tlist
 
-val fold_map   : (task_hd -> 'a * task -> ('a * task)) ->
-                                      'a -> task -> task trans
+val fold_map   : (task_hd -> 'a * 'b -> ('a * 'b)     ) -> 'a -> 'b -> 'b trans
+val fold_map_l : (task_hd -> 'a * 'b -> ('a * 'b) list) -> 'a -> 'b -> 'b tlist
 
-val fold_map_l : (task_hd -> 'a * task -> ('a * task) list) ->
-                                      'a -> task -> task tlist
-
-val decl   : (decl -> decl list     ) -> task -> task trans
 (** [decl f acc [d1;..;dn]] returns acc@f d1@..@f dn *)
+val decl   : (decl -> decl list     ) -> task -> task trans
 val decl_l : (decl -> decl list list) -> task -> task tlist
 
 val tdecl   : (decl -> tdecl list     ) -> task -> task trans

src/printer/cvc3.ml

@@ -303,7 +303,7 @@ let distingued =
     | _ -> assert false in
   Trans.on_meta meta_syntax_logic (fun syntax ->
     let syntax = List.fold_left dist_syntax Mls.empty syntax in
-    Trans.on_meta Encoding.meta_lsinst (fun dis ->
+    Trans.on_meta Encoding_distinction.meta_lsinst (fun dis ->
       let dis2 = List.fold_left (dist_dist syntax) Mid.empty dis in
       Trans.return dis2))
 

src/printer/smt2.ml

@@ -307,7 +307,7 @@ let distingued =
     | _ -> assert false in
   Trans.on_meta meta_syntax_logic (fun syntax ->
     let syntax = List.fold_left dist_syntax Mls.empty syntax in
-    Trans.on_meta Encoding.meta_lsinst (fun dis ->
+    Trans.on_meta Encoding_distinction.meta_lsinst (fun dis ->
       let dis2 = List.fold_left (dist_dist syntax) Mid.empty dis in
       Trans.return dis2))
 

src/transform/encoding.ml

@@ -17,92 +17,72 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Env
-open Theory
+open Util
+open Ident
 open Ty
+open Term
+open Decl
+open Theory
 open Task
 open Trans
-open Term
 
 let debug = Debug.register_flag "encoding"
 
-let meta_lsinst   = Encoding_distinction.meta_lsinst
-let meta_kept   = Encoding_distinction.meta_kept
-let meta_lskept = register_meta "encoding : lskept"    [MTlsymbol]
-let meta_base   = register_meta_excl "encoding : base" [MTtysymbol]
+let meta_kept = register_meta      "encoding : kept" [MTty]
+let meta_base = register_meta_excl "encoding : base" [MTtysymbol]
 
+let meta_select_kept = register_meta_excl "select_kept" [MTstring]
+let meta_enco_kept   = register_meta_excl "enco_kept"   [MTstring]
+let meta_enco_poly   = register_meta_excl "enco_poly"   [MTstring]
 
-let meta_select_lsinst   = register_meta_excl "select_inst"     [MTstring]
-let meta_select_kept     = register_meta_excl "select_kept"     [MTstring]
-let meta_select_lskept   = register_meta_excl "select_lskept"   [MTstring]
-let meta_completion_mode = register_meta_excl "completion_mode" [MTstring]
+let def_enco_select_smt  = "none"
+let def_enco_kept_smt    = "bridge"
+let def_enco_poly_smt    = "decorate"
 
-let meta_enco_kept       = register_meta_excl "enco_kept"       [MTstring]
-let meta_enco_poly       = register_meta_excl "enco_poly"       [MTstring]
-
-
-let def_enco_select_smt = "kept"
-let def_enco_kept_smt   = "bridge"
-let def_enco_poly_smt   = "decorate"
-
-let def_enco_select_tptp = "kept"
+let def_enco_select_tptp = "none"
 let def_enco_kept_tptp   = "bridge"
 let def_enco_poly_tptp   = "decorate"
 
-
-let ft_select_lsinst    = ((Hashtbl.create 17) : (env,task) Trans.flag_trans)
-let ft_select_kept      = ((Hashtbl.create 17) : (env,task) Trans.flag_trans)
-let ft_select_lskept    = ((Hashtbl.create 17) : (env,task) Trans.flag_trans)
-let ft_completion_mode  = ((Hashtbl.create 17) : (env,task) Trans.flag_trans)
-
-let ft_enco_kept   = ((Hashtbl.create 17) : (env,task) Trans.flag_trans)
-let ft_enco_poly   = ((Hashtbl.create 17) : (env,task) Trans.flag_trans)
-
-
-let monomorphise_goal =
-  Trans.goal (fun pr f ->
-    let stv = t_ty_freevars Stv.empty f in
-    let mty,ltv = Stv.fold (fun tv (mty,ltv) ->
-      let ts = create_tysymbol (Ident.id_clone tv.tv_name) [] None in
-      Mtv.add tv (ty_app ts []) mty,ts::ltv) stv (Mtv.empty,[]) in
-    let f = t_ty_subst mty Mvs.empty f in
-    let acc = [Decl.create_prop_decl Decl.Pgoal pr f] in
-    let acc = List.fold_left
-      (fun acc ts -> (Decl.create_ty_decl [ts,Decl.Tabstract]) :: acc)
-      acc ltv in
-    acc)
-
-
-let lsymbol_distinction =
-  Trans.seq
-    [Trans.print_meta debug meta_lskept;
-     Trans.print_meta debug meta_lsinst;
-     Encoding_distinction.lsymbol_distinction]
-
-let phase0 env = Trans.seq [
-  Trans.on_flag meta_select_lsinst   ft_select_lsinst   "nothing" env;
-  Trans.on_flag meta_select_kept     ft_select_kept     "nothing" env;
-  Trans.on_flag meta_select_lskept   ft_select_lskept   "nothing" env;
-  Trans.on_flag meta_completion_mode ft_completion_mode "nothing" env;
-  lsymbol_distinction;
-]
-
+let ft_select_kept = ((Hashtbl.create 17) : (Env.env,Sty.t) Trans.flag_trans)
+let ft_enco_kept   = ((Hashtbl.create 17) : (Env.env,task)  Trans.flag_trans)
+let ft_enco_poly   = ((Hashtbl.create 17) : (Env.env,task)  Trans.flag_trans)
+
+let monomorphise_goal = Trans.goal (fun pr f ->
+  let stv = t_ty_freevars Stv.empty f in
+  if Stv.is_empty stv then [create_prop_decl Pgoal pr f] else
+  let mty,ltv = Stv.fold (fun tv (mty,ltv) ->
+    let ts = create_tysymbol (id_clone tv.tv_name) [] None in
+    Mtv.add tv (ty_app ts []) mty, ts::ltv) stv (Mtv.empty,[]) in
+  let f = t_ty_subst mty Mvs.empty f in
+  List.fold_left
+    (fun acc ts -> create_ty_decl [ts,Tabstract] :: acc)
+    [create_prop_decl Pgoal pr f] ltv)
+
+let select_kept def env =
+  let select = Trans.on_flag meta_select_kept ft_select_kept def env in
+  let trans task =
+    let sty = Trans.apply select task in
+    let create_meta_ty ty = create_meta meta_kept [MAty ty] in
+    let decls = Sty.fold (flip $ cons create_meta_ty) sty [] in
+    Trans.apply (Trans.add_tdecls decls) task
+  in
+  Trans.store trans
 
 let encoding_smt env = Trans.seq [
   monomorphise_goal;
-  phase0 env;
+  select_kept def_enco_select_smt env;
   Trans.print_meta debug meta_kept;
   Trans.on_flag meta_enco_kept ft_enco_kept def_enco_kept_smt env;
   Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_smt env]
 
 let encoding_tptp env = Trans.seq [
   monomorphise_goal;
-  phase0 env;
+  select_kept def_enco_select_tptp env;
   Trans.print_meta debug meta_kept;
   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;
   Encoding_enumeration.encoding_enumeration]
 
-let () =
-  register_env_transform "encoding_smt" encoding_smt;
-  register_env_transform "encoding_tptp" encoding_tptp
+let () = register_env_transform "encoding_smt" encoding_smt
+let () = register_env_transform "encoding_tptp" encoding_tptp
+

src/transform/encoding.mli

@@ -17,27 +17,17 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Env
-open Theory
-open Task
-open Trans
-
 val debug : Debug.flag
 
-val meta_base          : Theory.meta
-val meta_lsinst        : Theory.meta
-val meta_kept          : Theory.meta
-val meta_lskept        : Theory.meta
-
-val ft_select_lsinst    : (env,task) Trans.flag_trans
-val ft_select_kept      : (env,task) Trans.flag_trans
-val ft_select_lskept    : (env,task) Trans.flag_trans
-val ft_completion_mode  : (env,task) Trans.flag_trans
+val meta_base : Theory.meta
+val meta_kept : Theory.meta
 
-val ft_enco_kept : (env,task) Trans.flag_trans
-val ft_enco_poly : (env,task) Trans.flag_trans
+val ft_select_kept : (Env.env,Ty.Sty.t)  Trans.flag_trans
+val ft_enco_kept   : (Env.env,Task.task) Trans.flag_trans
+val ft_enco_poly   : (Env.env,Task.task) Trans.flag_trans
 
 val monomorphise_goal : Task.task Trans.trans
 
 val encoding_smt  : Env.env -> Task.task Trans.trans
 val encoding_tptp : Env.env -> Task.task Trans.trans
+

src/transform/encoding_distinction.ml

@@ -25,36 +25,45 @@ open Decl
 open Theory
 open Task
 
+let meta_inst   = register_meta "encoding : inst"   [MTty]
+let meta_lskept = register_meta "encoding : lskept" [MTlsymbol]
+let meta_lsinst = register_meta "encoding : lsinst" [MTlsymbol;MTlsymbol]
 
-(** Transformation "distinction" *)
+let meta_select_inst   = register_meta_excl "select_inst"   [MTstring]
+let meta_select_lskept = register_meta_excl "select_lskept" [MTstring]
+let meta_select_lsinst = register_meta_excl "select_lsinst" [MTstring]
 
-let meta_lsinst = register_meta "encoding : lsinst" [MTlsymbol;MTlsymbol]
-let meta_kept   = register_meta "encoding : kept"   [MTty]
+module OHTy = OrderedHash(struct
+  type t = ty
+  let tag = ty_hash
+end)
 
-module Env = struct
+module OHTyl = OrderedHashList(struct
+  type t = ty
+  let tag = ty_hash
+end)
 
+module Mtyl = Stdlib.Map.Make(OHTyl)
+
+module Lsmap = struct
 
 (* TODO : transmettre les tags des logiques polymorphe vers les logiques
    instantié. Un tag sur un logique polymorphe doit être un tag sur toute
    la famille de fonctions *)
 
-  module OHTy = OrderedHash(struct
-    type t = ty
-    let tag = ty_hash
-  end)
-
-  module OHTyl = OrderedHashList(struct
-    type t = ty
-    let tag = ty_hash
-  end)
+  type t = lsymbol Mtyl.t Mls.t
 
-  module Mtyl = Map.Make(OHTyl)
-