libencoding.ml 9.64 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 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
(*    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 Util
open Ident
open Ty
open Term
open Decl

(* sort symbol of (polymorphic) types *)
let ts_type = create_tysymbol (id_fresh "ty") [] None

(* sort of (polymorphic) types *)
let ty_type = ty_app ts_type []

(* ts_type declaration *)
let d_ts_type = create_ty_decl [ts_type, Tabstract]

(* function symbol mapping ty_type^n to ty_type *)
let ls_of_ts = Wts.memoize 63 (fun ts ->
  let args = List.map (const ty_type) ts.ts_args in
  create_fsymbol (id_clone ts.ts_name) args ty_type)

40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71
(* function symbol selecting ty_type from ty_type^n *)
let ls_selects_of_ts = Wts.memoize 63 (fun ts ->
  let create_select _ =
    let preid = id_fresh ("select_"^ts.ts_name.id_string) in
    create_fsymbol preid [ty_type] ty_type in
  List.rev_map create_select ts.ts_args)

(** definition of the previous selecting functions *)
let ls_selects_def_of_ts acc ts =
  let ls = ls_of_ts ts in
  let ls_selects = ls_selects_of_ts ts in
  let vars = List.rev_map
    (fun _ -> create_vsymbol (id_fresh "x") ty_type) ls_selects
  in
  let tvars = List.map t_var vars in
  let fmlas = List.rev_map2
    (fun ls_select value ->
      let t = t_app ls tvars ty_type in
      let f = f_equ (t_app ls_select [t] ty_type) value in
      let f = f_forall_close vars [] f in
      f)
    ls_selects tvars in
  let create_props ls_select fmla =
    let prsymbol = create_prsymbol (id_clone ls_select.ls_name) in
    create_prop_decl Paxiom prsymbol fmla in
  let props =
    List.fold_left2 (fun acc x y -> create_props x y::acc)
      acc ls_selects fmlas in
  let add acc fs = create_logic_decl [fs,None] :: acc in
  List.fold_left add props ls_selects


72 73 74
(* convert a type to a term of type ty_type *)
let rec term_of_ty tvmap ty = match ty.ty_node with
  | Tyvar tv ->
75
      Mtv.find tv tvmap
76 77 78
  | Tyapp (ts,tl) ->
      t_app (ls_of_ts ts) (List.map (term_of_ty tvmap) tl) ty_type

79
(* rewrite a closed formula modulo its free typevars *)
François Bobot's avatar
François Bobot committed
80
let type_close tvs fn f =
81
  let get_vs tv = create_vsymbol (id_clone tv.tv_name) ty_type in
82 83 84
  let tvm = Mtv.mapi (fun v () -> get_vs v) tvs in
  let vl = Mtv.values tvm in
  let tvm = Mtv.map t_var tvm in
85 86
  f_forall_close_simp vl [] (fn tvm f)

François Bobot's avatar
François Bobot committed
87 88 89 90
let f_type_close fn f =
  let tvs = f_ty_freevars Stv.empty f in
  type_close tvs fn f

91
(* convert a type declaration to a list of lsymbol declarations *)
92
let lsdecl_of_tydecl acc td = match td with
93 94 95 96 97
    | ts, Talgebraic _ ->
        let ty = ty_app ts (List.map ty_var ts.ts_args) in
        Printer.unsupportedType ty "no algebraic types at this point"
    | { ts_def = Some _ }, _ -> acc
    | ts, _ -> create_logic_decl [ls_of_ts ts, None] :: acc
98 99 100 101 102 103 104 105 106 107 108



(* convert a type declaration to a list of lsymbol declarations *)
let lsdecl_of_tydecl_select tdl =
  let add acc td = match td with
    | ts, Talgebraic _ ->
        let ty = ty_app ts (List.map ty_var ts.ts_args) in
        Printer.unsupportedType ty "no algebraic types at this point"
    | { ts_def = Some _ }, _ -> acc
    | ts, _ -> ls_selects_def_of_ts acc ts
109
  in
110 111 112 113
  let defs = List.fold_left add [] tdl in
  List.fold_left lsdecl_of_tydecl defs tdl

let lsdecl_of_tydecl tdl = List.fold_left lsdecl_of_tydecl [] tdl
114 115

(* convert a constant to a functional symbol of type ty_base *)
116
let ls_of_const ty_base =
117
  let ht = Hterm.create 63 in
118
  fun t -> match t.t_node with
119 120
    | Tconst _ ->
        begin try Hterm.find ht t with Not_found ->
121
          let s = "const_" ^ Pp.string_of_wnl Pretty.print_term t in
122
          let ls = create_fsymbol (id_fresh s) [] ty_base in
123 124
          Hterm.add ht t ls;
          ls
125 126 127
        end
    | _ -> assert false

128 129 130 131 132 133
let ls_of_const =
  let ht = Hty.create 3 in
  fun ty -> try Hty.find ht ty with Not_found ->
    let fn = ls_of_const ty in
    Hty.add ht ty fn;
    fn
134 135 136

(* monomorphise modulo the set of kept types * and an lsymbol map *)

137
let vs_monomorph ty_base kept vs =
138 139
  if Sty.mem vs.vs_ty kept then vs else
  create_vsymbol (id_clone vs.vs_name) ty_base
140

141 142 143
let rec t_monomorph ty_base kept lsmap consts vmap t =
  let t_mono = t_monomorph ty_base kept lsmap consts in
  let f_mono = f_monomorph ty_base kept lsmap consts in
144 145 146
  t_label_copy t (match t.t_node with
    | Tvar v ->
        Mvs.find v vmap
147 148
    | Tconst _ when Sty.mem t.t_ty kept ->
        t
149 150
    | Tconst _ ->
        let ls = ls_of_const ty_base t in
151 152 153 154 155 156 157 158 159 160
        consts := Sls.add ls !consts;
        t_app ls [] ty_base
    | Tapp (fs,tl) ->
        let fs = lsmap fs in
        let ty = of_option fs.ls_value in
        t_app fs (List.map (t_mono vmap) tl) ty
    | Tif (f,t1,t2) ->
        t_if (f_mono vmap f) (t_mono vmap t1) (t_mono vmap t2)
    | Tlet (t1,b) ->
        let u,t2,close = t_open_bound_cb b in
161
        let v = vs_monomorph ty_base kept u in
162 163 164 165 166 167
        let t2 = t_mono (Mvs.add u (t_var v) vmap) t2 in
        t_let (t_mono vmap t1) (close v t2)
    | Tcase _ ->
        Printer.unsupportedTerm t "no match expressions at this point"
    | Teps b ->
        let u,f,close = f_open_bound_cb b in
168
        let v = vs_monomorph ty_base kept u in
169 170 171
        let f = f_mono (Mvs.add u (t_var v) vmap) f in
        t_eps (close v f))

172 173 174
and f_monomorph ty_base kept lsmap consts vmap f =
  let t_mono = t_monomorph ty_base kept lsmap consts in
  let f_mono = f_monomorph ty_base kept lsmap consts in
175 176 177 178 179 180 181
  f_label_copy f (match f.f_node with
    | Fapp (ps,[t1;t2]) when ls_equal ps ps_equ ->
        f_equ (t_mono vmap t1) (t_mono vmap t2)
    | Fapp (ps,tl) ->
        f_app (lsmap ps) (List.map (t_mono vmap) tl)
    | Fquant (q,b) ->
        let ul,tl,f1,close = f_open_quant_cb b in
182
        let vl = List.map (vs_monomorph ty_base kept) ul in
183 184 185 186 187 188 189 190 191 192 193 194 195 196
        let add acc u v = Mvs.add u (t_var v) acc in
        let vmap = List.fold_left2 add vmap ul vl in
        let tl = tr_map (t_mono vmap) (f_mono vmap) tl in
        f_quant q (close vl tl (f_mono vmap f1))
    | Fbinop (op,f1,f2) ->
        f_binary op (f_mono vmap f1) (f_mono vmap f2)
    | Fnot f1 ->
        f_not (f_mono vmap f1)
    | Ftrue | Ffalse ->
        f
    | Fif (f1,f2,f3) ->
        f_if (f_mono vmap f1) (f_mono vmap f2) (f_mono vmap f3)
    | Flet (t,b) ->
        let u,f1,close = f_open_bound_cb b in
197
        let v = vs_monomorph ty_base kept u in
198 199 200 201 202
        let f1 = f_mono (Mvs.add u (t_var v) vmap) f1 in
        f_let (t_mono vmap t) (close v f1)
    | Fcase _ ->
        Printer.unsupportedFmla f "no match expressions at this point")

203 204
let d_monomorph ty_base kept lsmap d =
  let kept = Sty.add ty_base kept in
205
  let consts = ref Sls.empty in
206 207
  let t_mono = t_monomorph ty_base kept lsmap consts in
  let f_mono = f_monomorph ty_base kept lsmap consts in
208 209 210 211 212 213
  let dl = match d.d_node with
    | Dtype tdl ->
        let add td acc = match td with
          | _, Talgebraic _ ->
              Printer.unsupportedDecl d "no algebraic types at this point"
          | { ts_def = Some _ }, _ -> acc
214
          | ts, _ when not (Sty.exists (ty_s_any (ts_equal ts)) kept) -> acc
215 216 217 218 219 220
          | _ -> create_ty_decl [td] :: acc
        in
        List.fold_right add tdl []
    | Dlogic ldl ->
        let conv (ls,ld) =
          let ls =
François Bobot's avatar
François Bobot committed
221
            if ls_equal ls ps_equ then ls else lsmap ls
222 223 224 225
          in
          match ld with
          | Some ld ->
              let ul,e = open_ls_defn ld in
226
              let vl = List.map (vs_monomorph ty_base kept) ul in
227 228 229
              let add acc u v = Mvs.add u (t_var v) acc in
              let vmap = List.fold_left2 add Mvs.empty ul vl in
              let e = match e with
230 231
                | Term t -> Term (t_mono vmap t)
                | Fmla f -> Fmla (f_mono vmap f)
232 233 234 235 236 237 238
              in
              make_ls_defn ls vl e
          | None ->
              ls, None
        in
        [create_logic_decl (List.map conv ldl)]
    | Dind idl ->
239
        let iconv (pr,f) = pr, f_mono Mvs.empty f in
240 241 242
        let conv (ls,il) = lsmap ls, List.map iconv il in
        [create_ind_decl (List.map conv idl)]
    | Dprop (k,pr,f) ->
243
        [create_prop_decl k pr (f_mono Mvs.empty f)]
244 245 246
  in
  let add ls acc = create_logic_decl [ls,None] :: acc in
  Sls.fold add !consts dl
247 248 249 250 251 252 253 254 255 256 257 258 259 260 261

(** close by subterm *)
let close_kept =
  Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
    let fold ty acc =
      let rec add acc ty = ty_fold add (Sty.add ty acc) ty in
      add acc ty in
    let kept' = Sty.fold fold kept kept in
    if kept == kept' then Trans.identity
    else
      let kept' = Sty.diff kept' kept in
      let fold ty acc =
        Theory.create_meta Encoding.meta_kept [Theory.MAty ty] :: acc in
      Trans.add_tdecls (Sty.fold fold kept' [])
  )