encoding.ml 3.4 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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 Stdlib
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]
Andrei Paskevich's avatar
Andrei Paskevich committed
19 20 21 22 23 24 25 26 27 28 29
  ~desc:"Specify@ the@ types@ to@ mark@ with@ 'encoding : kept':@;  \
    @[\
      - 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.@]\
    @]"

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@ \
30
            and@ the@ universal@ type@]@\
Andrei Paskevich's avatar
Andrei Paskevich committed
31 32
    @]"

33
let meta_enco_poly = register_meta_excl "enco_poly" [MTstring]
Andrei Paskevich's avatar
Andrei Paskevich committed
34 35
  ~desc:"Specify@ the@ type@ encoding@ transformation:@;  \
    @[\
36 37 38 39 40 41 42
      - @[<hov 2>tags: protect@ variables@ in@ equalities@ \
            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.@]\
Andrei Paskevich's avatar
Andrei Paskevich committed
43
    @]"
44

45
let def_enco_select_smt  = "none"
46
let def_enco_kept_smt    = "twin"
47 48
let def_enco_poly_smt    = "guards"
let def_enco_poly_tptp   = "tags"
49

50 51 52
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)
53 54 55 56

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

63 64 65 66 67
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

68
let encoding_smt env = Trans.seq [
69
  Libencoding.monomorphise_goal;
70
  select_kept def_enco_select_smt env;
71
  Trans.print_meta Libencoding.debug Libencoding.meta_kept;
72 73
  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]
74

75
let encoding_tptp env = Trans.seq [
76
  Libencoding.monomorphise_goal;
77 78
  forget_kept;
  Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_tptp env]
Francois Bobot's avatar
Francois Bobot committed
79

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

83
let () = register_env_transform "encoding_tptp" encoding_tptp
Andrei Paskevich's avatar
Andrei Paskevich committed
84
  ~desc:"Encode@ polymorphic@ types@ for@ provers@ without@ sorts."