update polymorphism encoding to the last technical report

in particular, there is no more need to define intermediate
sorts or to close the set of protected types wrt subtyping

Makefile.in

@@ -127,7 +127,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
 		eliminate_inductive eliminate_let eliminate_if \
 		libencoding discriminate protect_enumeration \
 		encoding encoding_select \
-		encoding_decorate encoding_bridge \
+		encoding_decorate encoding_bridge encoding_twin \
 		encoding_explicit encoding_guard encoding_sort \
 		encoding_instantiate simplify_array filter_trigger \
 		introduction abstraction close_epsilon lift_epsilon \

src/transform/encoding.ml

@@ -31,11 +31,11 @@ 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  = "none"
-let def_enco_kept_smt    = "bridge"
+let def_enco_kept_smt    = "twin"
 let def_enco_poly_smt    = "decorate"
 
 let def_enco_select_tptp = "none"
-let def_enco_kept_tptp   = "bridge"
+let def_enco_kept_tptp   = "twin"
 let def_enco_poly_tptp   = "decorate"
 
 let ft_select_kept = ((Hashtbl.create 17) : (Env.env,Sty.t) Trans.flag_trans)

src/transform/encoding_decorate.ml

@@ -31,19 +31,30 @@ 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_type t) kept then t else
+let decorate tvar t =
   let tty = term_of_ty tvar (t_type t) 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
-  | Tquant (q,b) ->
-      let vl,tl,f,close = t_open_quant_cb b in
-      let tl = TermTF.tr_map (deco_arg kept tvar) (deco_term kept tvar) tl in
-      t_quant q (close vl tl (deco_term kept tvar f))
-  | _ -> t_map (deco_term kept tvar) t
+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,_) ->
+        let t = t_map deco t in
+        if ls.ls_value = None || is_protected_ls kept ls
+        then t else decorate tvar t
+    | Tlet (t1,tb) ->
+        let v,e,close = t_open_bound_cb tb in
+        t_let (t_map deco t1) (close v (deco e))
+    | 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
+    | _ -> t_map deco t
+  in
+  deco
 
 let deco_decl kept d = match d.d_node with
   | Dtype tdl ->
@@ -77,8 +88,10 @@ 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 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_deco 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 = Util.option_map pos ls.ls_value in
   if Util.option_eq ty_equal tyr ls.ls_value

src/transform/encoding_decorate.mli

@@ -16,4 +16,3 @@
 (*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
 (*                                                                        *)
 (**************************************************************************)
-

src/transform/encoding_explicit.ml

@@ -144,9 +144,12 @@ let explicit =
 open Libencoding
 
 let lsmap kept = Wls.memoize 63 (fun ls ->
-  let tymap ty = if Sty.mem ty kept then ty else ty_base in
-  let ty_res = Util.option_map tymap ls.ls_value in
-  let ty_arg = List.map tymap ls.ls_args in
+  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 = Util.option_map pos ls.ls_value in
   if Util.option_eq 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)
@@ -160,4 +163,3 @@ let monomorph = Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
 
 let () = Hashtbl.replace Encoding.ft_enco_poly "explicit"
     (fun _ -> Trans.compose explicit monomorph)
-

src/transform/encoding_guard.ml

@@ -132,7 +132,7 @@ module Transform = struct
 
   and guard q kept varM fmla vsl =
     let aux fmla vs =
-      if Sty.mem vs.vs_ty kept then fmla else
+      if Libencoding.is_protected_vs kept vs then fmla else
         let g = t_equ (app_type (t_var vs)) (term_of_ty varM vs.vs_ty) in
         match q with
           | Tforall -> t_implies g fmla
@@ -173,10 +173,11 @@ module Transform = struct
   let logic_guard kept acc lsymbol =
     match lsymbol.ls_value with
       | None -> acc
-      | Some ty_val when Sty.mem ty_val kept -> acc
+      | Some _ when Libencoding.is_protected_ls kept lsymbol -> acc
       | Some ty_val ->
-        let varl = List.map (fun v -> create_vsymbol (id_fresh "x") v)
-          lsymbol.ls_args in
+        let v_id = if Libencoding.is_protecting_id lsymbol.ls_name
+          then id_fresh "x" else Libencoding.id_unprotected "j" in
+        let varl = List.map (create_vsymbol v_id) lsymbol.ls_args in
         let trans varM () =
           let terms = List.map t_var varl in
           let terms = args_transform kept varM lsymbol terms ty_val in
@@ -184,7 +185,7 @@ module Transform = struct
             t_equ (app_type (fs_app (findL lsymbol) terms ty_val))
               (term_of_ty varM ty_val) in
           let guard fmla vs =
-            if Sty.mem vs.vs_ty kept then fmla else
+            if Libencoding.is_protected_vs kept vs then fmla else
               let g = t_equ (app_type (t_var vs)) (term_of_ty varM vs.vs_ty) in
               t_implies g fmla in
           let fmla = List.fold_left guard fmla varl in
@@ -242,9 +243,12 @@ let guard =
 open Libencoding
 
 let lsmap kept = Wls.memoize 63 (fun ls ->
-  let tymap ty = if Sty.mem ty kept then ty else ty_base in
-  let ty_res = Util.option_map tymap ls.ls_value in
-  let ty_arg = List.map tymap ls.ls_args in
+  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 = Util.option_map pos ls.ls_value in
   if Util.option_eq 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)

src/transform/encoding_twin.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2011                                               *)
+(*    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        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Util
+open Ident
+open Ty
+open Term
+open Task
+open Theory
+open Task
+open Decl
+open Encoding
+
+type tenv = {
+  kept : Sty.t;
+  pont : (lsymbol * lsymbol) Mty.t; (* t2tb, tb2t *)
+  seen : unit Hty.t;
+  next : unit Hty.t;
+}
+
+let add_pont ty pont =
+  let t2tb =
+    let t2tb_name = "t2tb" in
+    let t2tb_id = Libencoding.id_unprotected t2tb_name in
+    create_fsymbol t2tb_id [ty] ty in
+  let tb2t =
+    let tb2t_name = "tb2t" in
+    let tb2t_id = Libencoding.id_unprotecting tb2t_name in
+    create_fsymbol tb2t_id [ty] ty in
+  Mty.add ty (t2tb,tb2t) pont
+
+let make_tenv kept = {
+  kept = kept;
+  pont = Sty.fold add_pont kept Mty.empty;
+  seen = Hty.create 7;
+  next = Hty.create 7 }
+
+let add_decls tenv ty () decls =
+  if Hty.mem tenv.seen ty then decls else
+  let () = Hty.add tenv.seen ty () in
+  let (t2tb,tb2t) = Mty.find ty tenv.pont in
+  let t2tb_def = create_logic_decl [t2tb,None] in
+  let tb2t_def = create_logic_decl [tb2t,None] in
+  let bridge_l =
+    let x_vs = create_vsymbol (id_fresh "i") ty in
+    let x_t = t_var x_vs in
+    let t2tb_x = fs_app t2tb [x_t] ty in
+    let tb2t_t2tb_x = fs_app tb2t [t2tb_x] ty in
+    let eq = t_equ tb2t_t2tb_x x_t in
+    let ax = t_forall_close [x_vs] [[t2tb_x]] eq in
+    let pr = create_prsymbol (id_fresh "BridgeL") in
+    create_prop_decl Paxiom pr ax in
+  let bridge_r =
+    let x_vs = create_vsymbol (Libencoding.id_unprotected "j") ty in
+    let x_t = t_var x_vs in
+    let tb2t_x = fs_app tb2t [x_t] ty in
+    let t2tb_tb2t_x = fs_app t2tb [tb2t_x] ty in
+    let eq = t_equ t2tb_tb2t_x x_t in
+    let ax = t_forall_close [x_vs] [[t2tb_tb2t_x]] eq in
+    let pr = create_prsymbol (id_fresh "BridgeR") in
+    create_prop_decl Paxiom pr ax in
+  t2tb_def :: tb2t_def :: bridge_l :: bridge_r :: decls
+
+let add_decls tenv decls =
+  let decls = Hty.fold (add_decls tenv) tenv.next decls in
+  Hty.clear tenv.next;
+  decls
+
+let conv_arg tenv t aty =
+  let tty = t_type t in
+  if ty_equal tty aty then t else
+  try
+    let (t2tb,tb2t) = Mty.find tty tenv.pont in
+    Hty.replace tenv.next tty ();
+    match t.t_node with
+      | Tapp (fs,[t]) when ls_equal fs tb2t -> t
+      | _ -> fs_app t2tb [t] tty
+  with Not_found -> t
+
+let conv_app tenv fs tl tty =
+  let t = fs_app fs tl tty in
+  let vty = Util.of_option fs.ls_value in
+  if ty_equal tty vty then t else
+  try
+    let (_,tb2t) = Mty.find tty tenv.pont in
+    Hty.replace tenv.next tty ();
+    fs_app tb2t [t] tty
+  with Not_found -> t
+
+(* FIXME? in quantifiers we might generate triggers
+   with unnecessary bridge functions over them *)
+let rec rewrite tenv t = match t.t_node with
+  | Tapp (ls,[t1;t2]) when ls_equal ls ps_equ ->
+      t_equ (rewrite tenv t1) (rewrite tenv t2)
+  | Tapp (ls,tl) ->
+      let tl = List.map (rewrite tenv) tl in
+      let tl = List.map2 (conv_arg tenv) tl ls.ls_args in
+      if t.t_ty = None then ps_app ls tl
+      else conv_app tenv ls tl (t_type t)
+  | _ -> t_map (rewrite tenv) t
+
+let decl tenv d = match d.d_node with
+  | Dtype [_,Tabstract] -> [d]
+  | Dtype _ -> Printer.unsupportedDecl d
+      "Algebraic and recursively-defined types are \
+            not supported, run eliminate_algebraic"
+  | Dlogic [_, None] -> [d]
+  | Dlogic [ls, Some ld] when not (Sid.mem ls.ls_name d.d_syms) ->
+      let f = rewrite tenv (ls_defn_axiom ld) in
+      Libencoding.defn_or_axiom 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 (rewrite tenv f)]
+
+let decl tenv d =
+  let decls = decl tenv d in
+  add_decls tenv decls
+
+let t = Trans.on_tagged_ty Libencoding.meta_kept (fun s ->
+  Trans.decl (decl (make_tenv s)) None)
+
+let () = Hashtbl.replace Encoding.ft_enco_kept "twin" (const t)
+

src/transform/encoding_twin.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-2011                                               *)
+(*    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        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)

src/transform/libencoding.ml

@@ -150,10 +150,27 @@ let ls_of_const =
         end
     | _ -> assert false
 
+(* unprotected and unprotecting idents *)
+
+let unprotected_label = "encoding : unprotected"
+let unprotecting_label = "encoding : unprotecting"
+
+let id_unprotected n = id_fresh ~label:[unprotected_label] n
+let id_unprotecting n = id_fresh ~label:[unprotecting_label] n
+
+let is_protected_id id = not (List.mem unprotected_label id.id_label)
+let is_protecting_id id = not (List.mem unprotecting_label id.id_label)
+
+let is_protected_vs kept vs =
+  is_protected_id vs.vs_name && Sty.mem vs.vs_ty kept
+
+let is_protected_ls kept ls =
+  is_protected_id ls.ls_name && Sty.mem (of_option ls.ls_value) kept
+
 (* monomorphise modulo the set of kept types * and an lsymbol map *)
 
 let vs_monomorph kept vs =
-  if Sty.mem vs.vs_ty kept then vs else
+  if is_protected_vs kept vs then vs else
   create_vsymbol (id_clone vs.vs_name) ty_base
 
 let rec t_monomorph kept lsmap consts vmap t =

src/transform/libencoding.mli

@@ -68,6 +68,18 @@ val lsdecl_of_tydecl : ty_decl list -> decl list
 (* convert a type declaration to a list of lsymbol declarations *)
 val lsdecl_of_tydecl_select : ty_decl list -> decl list
 
+(* a pre-id for vsymbols and lsymbols that produce non-kept values *)
+val id_unprotected : string -> Ident.preid
+val is_protected_id : Ident.ident -> bool
+
+(* a pre-id for lsymbols that treat their arguments as non-kept *)
+val id_unprotecting : string -> Ident.preid
+val is_protecting_id : Ident.ident -> bool
+
+(* the value type is in kept and the ident is not unprotected *)
+val is_protected_vs : Sty.t -> vsymbol -> bool
+val is_protected_ls : Sty.t -> lsymbol -> bool
+
 (* monomorphise wrt the set of kept types, and a symbol map *)
 val d_monomorph : Sty.t -> (lsymbol -> lsymbol) -> decl -> decl list