encoding.ml 4.17 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
4
5
6
7
8
9
10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   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.                           *)
(*                                                                  *)
(********************************************************************)
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]
19
20
21
22
23
24
25
26
27
  ~desc:"@[Specify@ how@ to@ automatically@ choose@ the@ type@ that@ are@ \
           kept@ (mark@ by@ 'encoding : kept')@ by@ the@ polymorphic@ \
           encoding:@]@\n  \
@[\
  - none:@[ don't@ mark@ automatically@]@\n\
  - goal:@[ mark@ all@ the@ closed@ type@ that@ appear@ has@ argument@ \
            in@ the@ goal@]@\n\
  - all:@[ same@ as@ goal@ but@ also@ in@ the@ premises.@]\
@]"
28
let meta_enco_kept   = register_meta_excl "enco_kept"   [MTstring]
29
30
31
32
33
34
35
36
  ~desc:"@[Specify@ how@ to@ keep@ type:@]@\n  \
@[\
  - @[<hov 2>twin: use@ conversion@ function@ between@ the@ kept@ types@ \
              and@ the@ universal@ type (a complete encoding)@]@\n\
  - @[<hov 2>instantiate: instantiate all the axioms with the kept types@]@\n\
  - @[<hov 2>instantiate_complete: same@ as@ instantiate@ but@ keep@ a@ \
    version@ not@ instantiated(a@ complete@ encoding).@]\
@]"
37
let meta_enco_poly   = register_meta_excl "enco_poly"   [MTstring]
38
39
40
41
42
43
44
45
46
47
  ~desc:"@[Specify@ how@ to@ keep@ encode@ polymorphism:@]@\n  \
@[\
  - @[<hov 2>decoexp: TODO @]@\n\
  - @[<hov 2>decorate: add@ around@ all@ the@ terms@ a@ function@ which@ \
             give@ the@ type@ of@ the@ terms@]@\n\
  - @[<hov 2>guard: add@ guards@ (hypothesis)@ in@ all@ the@ axioms@ about@ \
             the@ type@ of@ the@ variables@]@\n\
  - @[<hov 2>explicit: add@ type@ argument@ to@ all@ the@ polymorphic@ \
             functions@]\
@]"
48

49
let def_enco_select_smt  = "none"
50
let def_enco_kept_smt    = "twin"
51
let def_enco_poly_smt    = "decorate"
52

53
let def_enco_select_tptp = "none"
54
let def_enco_kept_tptp   = "twin"
55
let def_enco_poly_tptp   = "decorate"
56

57
58
59
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)
60
61
62
63

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

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

77
let encoding_tptp env = Trans.seq [
78
  Libencoding.monomorphise_goal;
79
  select_kept def_enco_select_tptp env;
80
  Trans.print_meta Libencoding.debug Libencoding.meta_kept;
81
82
  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;
83
  Protect_finite.protect_finite]
Francois Bobot's avatar
Francois Bobot committed
84

85
let () = register_env_transform "encoding_smt" encoding_smt
86
87
88
89
90
  ~desc_metas:[meta_select_kept, Pp.empty_formatted;
               meta_enco_kept, Pp.empty_formatted;
               meta_enco_poly, Pp.empty_formatted]
  ~desc:"encode@ polymorphism@ with@ default@ configuration@ choosed@ for@ \
         smt@ solver"
91
let () = register_env_transform "encoding_tptp" encoding_tptp
92
93
94
95
96
  ~desc_metas:[meta_select_kept, Pp.empty_formatted;
               meta_enco_kept, Pp.empty_formatted;
               meta_enco_poly, Pp.empty_formatted]
  ~desc:"encode@ polymorphism@ with@ default@ configuration@ choosed@ for@ \
         tptp@ solver"