encoding.ml 4.42 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
(*    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
22
open Ty
Francois Bobot's avatar
Francois Bobot committed
23 24
open Task
open Trans
25
open Term
Francois Bobot's avatar
Francois Bobot committed
26

27 28
let debug = Debug.register_flag "encoding"

29 30 31 32 33 34 35 36 37 38 39 40 41 42
let meta_lsinst   = Encoding_distinction.meta_lsinst
let meta_kept   = Encoding_distinction.meta_kept
let meta_lskept = register_meta "encoding : lskept"    [MTlsymbol]
let meta_base   = register_meta_excl "encoding : base" [MTtysymbol]


let meta_select_lsinst   = register_meta_excl "select_inst"     [MTstring]
let meta_select_kept     = register_meta_excl "select_kept"     [MTstring]
let meta_select_lskept   = register_meta_excl "select_lskept"   [MTstring]
let meta_completion_mode = register_meta_excl "completion_mode" [MTstring]

let meta_enco_kept       = register_meta_excl "enco_kept"       [MTstring]
let meta_enco_poly       = register_meta_excl "enco_poly"       [MTstring]

Francois Bobot's avatar
Francois Bobot committed
43

44 45 46
let def_enco_select_smt = "kept"
let def_enco_kept_smt   = "bridge"
let def_enco_poly_smt   = "decorate"
Francois Bobot's avatar
Francois Bobot committed
47

48 49 50
let def_enco_select_tptp = "kept"
let def_enco_kept_tptp   = "bridge"
let def_enco_poly_tptp   = "decorate"
51

52 53 54 55 56 57

let ft_select_lsinst    = ((Hashtbl.create 17) : (env,task) Trans.flag_trans)
let ft_select_kept      = ((Hashtbl.create 17) : (env,task) Trans.flag_trans)
let ft_select_lskept    = ((Hashtbl.create 17) : (env,task) Trans.flag_trans)
let ft_completion_mode  = ((Hashtbl.create 17) : (env,task) Trans.flag_trans)

58 59
let ft_enco_kept   = ((Hashtbl.create 17) : (env,task) Trans.flag_trans)
let ft_enco_poly   = ((Hashtbl.create 17) : (env,task) Trans.flag_trans)
Francois Bobot's avatar
Francois Bobot committed
60

61 62 63

let monomorphise_goal =
  Trans.goal (fun pr f ->
64
    let stv = f_ty_freevars Stv.empty f in
65 66 67 68 69 70 71 72 73 74
    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)

75 76

let lsymbol_distinction =
77 78 79 80
  Trans.seq
    [Trans.print_meta debug meta_lskept;
     Trans.print_meta debug meta_lsinst;
     Encoding_distinction.lsymbol_distinction]
81 82 83 84 85 86 87 88 89 90

let phase0 env = Trans.seq [
  Trans.on_flag meta_select_lsinst   ft_select_lsinst   "nothing" env;
  Trans.on_flag meta_select_kept     ft_select_kept     "nothing" env;
  Trans.on_flag meta_select_lskept   ft_select_lskept   "nothing" env;
  Trans.on_flag meta_completion_mode ft_completion_mode "nothing" env;
  lsymbol_distinction;
]


91 92
let encoding_smt env = Trans.seq [
  monomorphise_goal;
93
  phase0 env;
94 95 96
  Trans.print_meta debug meta_kept;
  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]
97

98 99
let encoding_tptp env = Trans.seq [
  monomorphise_goal;
100
  phase0 env;
101 102 103 104
  Trans.print_meta debug meta_kept;
  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;
  Encoding_enumeration.encoding_enumeration]
Francois Bobot's avatar
Francois Bobot committed
105 106 107 108

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