encoding.ml 4.32 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
Francois Bobot's avatar
Francois Bobot committed
11

12
open Wstdlib
13
open Ty
14
open Theory
Francois Bobot's avatar
Francois Bobot committed
15 16 17
open Task
open Trans

18
let meta_select_kept = register_meta_excl "select_kept" [MTstring]
19
  ~desc:"Specify@ the@ types@ to@ mark@ with@ 'encoding:kept':@;  \
Andrei Paskevich's avatar
Andrei Paskevich committed
20 21 22 23 24 25
    @[\
      - none: @[don't@ mark@ any@ type@ automatically@]@\n\
      - goal: @[mark@ every@ closed@ type@ in@ the@ goal@]@\n\
      - all:  @[mark@ every@ closed@ type@ in@ the@ task.@]\
    @]"

26 27 28 29
let meta_select_kept_default =
  register_meta_excl "select_kept_default" [MTstring]
  ~desc:"Default@ setting@ for@ select_kept"

Andrei Paskevich's avatar
Andrei Paskevich committed
30 31 32 33
let meta_enco_kept = register_meta_excl "enco_kept" [MTstring]
  ~desc:"Specify@ the@ type@ protection@ transformation:@;  \
    @[\
      - @[<hov 2>twin: use@ conversion@ functions@ between@ the@ kept@ types@ \
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
34
            and@ the@ universal@ type@]\
Andrei Paskevich's avatar
Andrei Paskevich committed
35 36
    @]"

37
let meta_enco_poly = register_meta_excl "enco_poly" [MTstring]
Andrei Paskevich's avatar
Andrei Paskevich committed
38 39
  ~desc:"Specify@ the@ type@ encoding@ transformation:@;  \
    @[\
40 41 42
      - @[<hov 2>tags: protect@ variables@ in@ equalities@ \
            with@ type@ annotations@]@\n\
      - @[<hov 2>guards: protect@ variables@ in@ equalities@ \
43
            with@ type@ conditions@]@\n\
44 45 46
      - @[<hov 2>tags_full: put@ type@ annotations@ on@ top@ \
            of@ every@ term@]@\n\
      - @[<hov 2>guards_full: add@ type@ conditions@ for@ every@ variable.@]\
Andrei Paskevich's avatar
Andrei Paskevich committed
47
    @]"
48

49
let def_enco_select_smt  = "none"
50
let def_enco_kept_smt    = "twin"
51 52
let def_enco_poly_smt    = "guards"
let def_enco_poly_tptp   = "tags"
53

54 55 56
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_poly   = ((Hstr.create 17) : (Env.env,task)  Trans.flag_trans)
57 58

let select_kept def env =
59 60
  let def = Trans.on_flag meta_select_kept_default ft_select_kept def in
  let select = Trans.on_flag_t meta_select_kept ft_select_kept def env in
61
  let trans task =
62 63
    let add ty acc = create_meta Libencoding.meta_kept [MAty ty] :: acc in
    let decls = Sty.fold add (Trans.apply select task) [] in
64 65 66
    Trans.apply (Trans.add_tdecls decls) task
  in
  Trans.store trans
67

68 69 70 71 72
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

73
let encoding_smt env = Trans.seq [
74
  Libencoding.monomorphise_goal;
75
  select_kept def_enco_select_smt env;
76
  Trans.print_meta Libencoding.debug Libencoding.meta_kept;
77
  Trans.trace_goal "meta_enco_kept" (Trans.on_flag meta_enco_kept ft_enco_kept def_enco_kept_smt env);
78
  Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_smt env]
79

80
let encoding_tptp env = Trans.seq [
81
  Libencoding.monomorphise_goal;
82 83
  forget_kept;
  Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_tptp env]
Francois Bobot's avatar
Francois Bobot committed
84

85
let () = register_env_transform "encoding_smt" encoding_smt
Andrei Paskevich's avatar
Andrei Paskevich committed
86
  ~desc:"Encode@ polymorphic@ types@ for@ provers@ with@ sorts."
87

88
let () = register_env_transform "encoding_tptp" encoding_tptp
Andrei Paskevich's avatar
Andrei Paskevich committed
89
  ~desc:"Encode@ polymorphic@ types@ for@ provers@ without@ sorts."
90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114


(* encoding only if polymorphism occurs *)

let encoding_smt_if_poly env =
  Trans.on_meta Detect_polymorphism.meta_monomorphic_types_only
    (function
    | [] -> encoding_smt env
    | _ -> Trans.identity)

let () =
  Trans.register_env_transform "encoding_smt_if_poly"
    encoding_smt_if_poly
    ~desc:"Same@ as@ encoding_smt@ but@ only@ if@ polymorphism@ appear."

let encoding_tptp_if_poly env =
  Trans.on_meta Detect_polymorphism.meta_monomorphic_types_only
    (function
    | [] -> encoding_tptp env
    | _ -> Trans.identity)

let () =
  Trans.register_env_transform "encoding_tptp_if_poly"
    encoding_tptp_if_poly
    ~desc:"Same@ as@ encoding_tptp@ but@ only@ if@ polymorphism@ appear."