encoding.ml 3.83 KB
Newer Older
Francois Bobot's avatar
Francois Bobot committed
1
2
3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4
5
6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
Francois Bobot's avatar
Francois Bobot committed
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
(*    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 Env
open Theory
open Task
open Trans

François Bobot's avatar
François Bobot committed
25
let meta_kept = register_meta "encoding : kept" [MTty]
26
let meta_kept_array = register_meta "encoding : kept_array" [MTty]
27
let meta_base = register_meta_excl "encoding : base" [MTtysymbol]
Francois Bobot's avatar
Francois Bobot committed
28

29
30
let debug = Debug.register_flag "encoding"

Francois Bobot's avatar
Francois Bobot committed
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
type enco_opt =
    { meta : meta;
      default : string;
      table : (string,env -> task trans) Hashtbl.t}

let enco_opt s d =
  let table = Hashtbl.create 17 in
  { meta = register_meta_excl (Format.sprintf "enco_%s" s) [MTstring];
    table = table;
    default = d},
  Hashtbl.add table

let select_opt,register_enco_select = enco_opt "select" "kept"
let kept_opt,register_enco_kept = enco_opt "kept" "bridge"
let poly_opt,register_enco_poly = enco_opt "poly" "decorate"

47
let poly_smt_opt = poly_opt
48
let poly_tptp_opt = poly_opt
49

Francois Bobot's avatar
Francois Bobot committed
50
let enco_gen opt env =
51
52
  Trans.on_meta_excl opt.meta (fun alo ->
    let s = match alo with
Francois Bobot's avatar
Francois Bobot committed
53
54
55
56
      | None -> opt.default
      | Some [MAstr s] -> s
      | _ -> assert false in
    try
57
      Trans.named s ((Hashtbl.find opt.table s) env)
Francois Bobot's avatar
Francois Bobot committed
58
    with Not_found -> failwith
59
      (Format.sprintf "encoding : %s wrong argument %s" opt.meta.meta_name s))
Francois Bobot's avatar
Francois Bobot committed
60

61
62
let print_kept = print_meta debug meta_kept
let enco_select env = compose (enco_gen select_opt env) print_kept
Francois Bobot's avatar
Francois Bobot committed
63
let enco_kept = enco_gen kept_opt
64
65
66
let enco_poly_smt = enco_gen poly_smt_opt
let enco_poly_tptp = enco_gen poly_tptp_opt

Francois Bobot's avatar
Francois Bobot committed
67

68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
open Ty
open Term

let ty_all_quant =
  let rec add_vs s ty = match ty.ty_node with
    | Tyvar vs -> Stv.add vs s
    | _ -> ty_fold add_vs s ty in
  f_ty_fold add_vs Stv.empty

let monomorphise_goal =
  Trans.goal (fun pr f ->
    let stv = ty_all_quant 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 = f_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 encoding_smt env =
  compose monomorphise_goal
92
93
    (compose (enco_select env)
       (compose (enco_kept env) (enco_poly_smt env)))
94
95
96

let encoding_tptp env =
  compose monomorphise_goal
97
98
99
100
    (compose (enco_select env)
       (compose (enco_kept env)
          (compose (enco_poly_tptp env)
             Encoding_enumeration.encoding_enumeration)))
Francois Bobot's avatar
Francois Bobot committed
101
102
103
104

let () =
  register_env_transform "encoding_smt" encoding_smt;
  register_env_transform "encoding_tptp" encoding_tptp