encoding_explicit.ml 7.17 KB
Newer Older
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é                                                      *)
7 8 9 10 11 12 13 14 15 16 17 18 19
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

Francois Bobot's avatar
Francois Bobot committed
20
(** transformation from polymorphic logic to untyped logic. The polymorphic
21 22 23
logic must not have finite support types. *)


24 25 26 27 28 29
open Util
open Ident
open Ty
open Term
open Decl
open Task
30
open Libencoding
31

32 33 34 35 36
(** module with printing functions *)
module Debug = struct
  let print_mtv vprinter fmter m =
    Mtv.iter (fun key value -> Format.fprintf fmter "@[%a@] -> @[%a@]@."
      Pretty.print_tv key vprinter value) m
Simon Cruanes's avatar
Simon Cruanes committed
37

38 39 40
  (** utility to print a list of items *)
  let rec print_list printer fmter = function
    | [] -> Format.fprintf fmter ""
41 42 43 44 45
    | e::es ->
      if es = [] then
        Format.fprintf fmter "@[%a@] %a" printer e (print_list printer) es
      else
        Format.fprintf fmter "@[%a@], %a" printer e (print_list printer) es
46 47 48

  let debug x = Format.eprintf "%s@." x
end
49

Simon Cruanes's avatar
Simon Cruanes committed
50 51
(** {2 module to separate utilities from important functions} *)

52 53
module Transform = struct

54 55
  (** creates a new logic symbol, with a different type if the
  given symbol was polymorphic *)
56
  let findL = Wls.memoize 63 (fun lsymbol ->
57
    if ls_equal lsymbol ps_equ then lsymbol else
58
    let new_ty = ls_ty_freevars lsymbol in
59
    (* as many t as type vars *)
60
    if Stv.is_empty new_ty then lsymbol (* same type *) else
61
      let add _ acc = ty_type :: acc in
62
      let args = Stv.fold add new_ty lsymbol.ls_args in
63
      (* creates a new lsymbol with the same name but a different type *)
64
      Term.create_lsymbol (id_clone lsymbol.ls_name) args lsymbol.ls_value)
65

66 67 68
  (** {1 transformations} *)

  (** translation of terms *)
69
  let rec term_transform varM t = match t.t_node with
70
    | Tapp(f, terms) ->
71
      let terms = args_transform varM f terms t.t_ty in
72
      t_app (findL f) terms t.t_ty
73
    | _ -> (* default case : traverse *)
74
      TermTF.t_map (term_transform varM) (fmla_transform varM) t
75

76
  (** translation of formulae *)
77
  and fmla_transform varM f = match f.t_node with
78
      (* first case : predicate (not =), we must translate it and its args *)
79
    | Tapp(p,terms) when not (ls_equal p ps_equ) ->
80
      let terms = args_transform varM p terms None in
81
      ps_app (findL p) terms
82
    | _ -> (* otherwise : just traverse and translate *)
83
      TermTF.t_map (term_transform varM) (fmla_transform varM) f
84

85
  and args_transform varM ls args ty =
86 87 88
    (* Debug.print_list Pretty.print_ty Format.std_formatter type_vars; *)
    let tv_to_ty = ls_app_inst ls args ty in
    (* Debug.print_mtv Pretty.print_ty Format.err_formatter tv_to_ty; *)
89
    let args = List.map (term_transform varM) args in
90
    (* fresh args to be added at the beginning of the list of arguments *)
91
    let add _ ty acc = term_of_ty varM ty :: acc in
92 93
    Mtv.fold add tv_to_ty args

94
  (** transforms a list of logic declarations into another.
95 96
  Declares new lsymbols with explicit polymorphic signatures. *)
  let logic_transform decls =
97
    (* if there is a definition, we must take it into account *)
98
    let helper = function
99
    | (lsymbol, Some ldef) ->
100
      let new_lsymbol = findL lsymbol in (* new lsymbol *)
101
      let vars,expr = open_ls_defn ldef in
102
      let add v (vl,vm) =
103
        let vs = Term.create_vsymbol (id_fresh "t") ty_type in
104
        vs :: vl, Mtv.add v (t_var vs) vm
105 106
      in
      let vars,varM = Stv.fold add (ls_ty_freevars lsymbol) (vars,Mtv.empty) in
Andrei Paskevich's avatar
Andrei Paskevich committed
107 108 109
      (match expr.t_ty with
      | Some _ ->
          let t = term_transform varM expr in
110
          Decl.make_ls_defn new_lsymbol vars t
Andrei Paskevich's avatar
Andrei Paskevich committed
111 112
      | None ->
          let f = fmla_transform varM expr in
113
          Decl.make_ls_defn new_lsymbol vars f)
114
    | (lsymbol, None) ->
115 116 117
      (findL lsymbol, None)
    in
    [Decl.create_logic_decl (List.map helper decls)]
118

119 120
  (** transform an inductive declaration *)
  let ind_transform idl =
121
    let iconv (pr,f) = pr, Libencoding.f_type_close fmla_transform f in
122 123 124 125
    let conv (ls,il) = findL ls, List.map iconv il in
    [Decl.create_ind_decl (List.map conv idl)]

  (** transforms a proposition into another (mostly a substitution) *)
126 127
  let prop_transform (prop_kind, prop_name, f) =
    let quantified_fmla = Libencoding.f_type_close fmla_transform f in
128
    [Decl.create_prop_decl prop_kind prop_name quantified_fmla]
129

130
end
131

Simon Cruanes's avatar
Simon Cruanes committed
132 133
(** {2 main part} *)

134 135 136 137 138 139 140 141
let decl d = match d.d_node with
  | Dtype tdl -> d :: Libencoding.lsdecl_of_tydecl tdl
  | Dlogic ldl -> Transform.logic_transform ldl
  | Dind idl -> Transform.ind_transform idl
  | Dprop prop -> Transform.prop_transform prop

let explicit = Trans.decl decl (Task.add_decl None d_ts_type)

142 143 144 145 146 147 148 149 150
let meta_enum = Eliminate_algebraic.meta_enum

let explicit =
  Trans.on_tagged_ts meta_enum (fun enum ->
    if Sts.is_empty enum then explicit
    else Printer.unsupportedTysymbol (Sts.choose enum)
      "explicit is unsound in presence of type")


151 152
(** {2 monomorphise task } *)

153 154 155 156 157
let ts_base = create_tysymbol (id_fresh "uni") [] None
let ty_base = ty_app ts_base []

let lsmap tyb kept = Wls.memoize 63 (fun ls ->
  let tymap ty = if Sty.mem ty kept then ty else tyb in
158 159 160 161 162 163
  let ty_res = Util.option_map tymap ls.ls_value in
  let ty_arg = List.map tymap ls.ls_args in
  if Util.option_eq ty_equal ty_res ls.ls_value &&
     List.for_all2 ty_equal ty_arg ls.ls_args then ls
  else create_lsymbol (id_clone ls.ls_name) ty_arg ty_res)

164 165
let d_ts_base = create_ty_decl [ts_base, Tabstract]

François Bobot's avatar
François Bobot committed
166 167
let monomorph tyb = Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
  let kept = Sty.add ty_type kept in
168 169 170 171 172
  let tyb = match tyb.ty_node with
    | Tyapp (_,[]) when not (Sty.mem tyb kept) -> tyb
    | _ -> ty_base
  in
  let decl = Libencoding.d_monomorph tyb kept (lsmap tyb kept) in
173 174
  Trans.decl decl (Task.add_decl None d_ts_base))

175 176
let monomorph = Trans.on_meta_excl Encoding.meta_base (fun alo ->
  let tyb = match alo with
177 178 179 180 181 182 183 184 185
    | Some [Theory.MAts ts] when ts.ts_args = [] ->
        begin match ts.ts_def with
          | Some ty -> ty
          | None -> ty_app ts []
        end
    | _ -> ty_base
  in
  monomorph tyb)

186
let () = Hashtbl.replace Encoding.ft_enco_poly "explicit"
187
    (fun _ -> Trans.compose explicit monomorph)
188