libencoding.ml 10.1 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
(* 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)

47 48
let ls_int_of_ty = create_fsymbol (id_fresh "int_of_ty") [ty_type] ty_int

49 50 51 52
(** definition of the previous selecting functions *)
let ls_selects_def_of_ts acc ts =
  let ls = ls_of_ts ts in
  let vars = List.rev_map
53
    (fun _ -> create_vsymbol (id_fresh "x") ty_type) ts.ts_args
54 55
  in
  let tvars = List.map t_var vars in
56 57 58 59 60
  (** type to int *)
  let id = string_of_int (id_hash ts.ts_name) in
  let acc =
    let t = t_app ls tvars ty_type in
    let f = f_equ (t_app ls_int_of_ty [t] ty_int) (t_int_const id) in
Andrei Paskevich's avatar
Andrei Paskevich committed
61
    let f = f_forall_close vars [[t]] f in
62 63 64 65 66
    let prsymbol = create_prsymbol (id_clone ts.ts_name) in
    create_prop_decl Paxiom prsymbol f :: acc
  in
  (** select *)
  let ls_selects = ls_selects_of_ts ts in
67 68 69
  let fmlas = List.rev_map2
    (fun ls_select value ->
      let t = t_app ls tvars ty_type in
70 71
      let t = t_app ls_select [t] ty_type in
      let f = f_equ t value in
Andrei Paskevich's avatar
Andrei Paskevich committed
72
      let f = f_forall_close vars [[t]] f in
73 74 75 76 77 78 79 80 81 82 83 84
      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


85 86 87
(* convert a type to a term of type ty_type *)
let rec term_of_ty tvmap ty = match ty.ty_node with
  | Tyvar tv ->
88
      Mtv.find tv tvmap
89 90 91
  | Tyapp (ts,tl) ->
      t_app (ls_of_ts ts) (List.map (term_of_ty tvmap) tl) ty_type

92
(* rewrite a closed formula modulo its free typevars *)
François Bobot's avatar
François Bobot committed
93
let type_close tvs fn f =
94
  let get_vs tv = create_vsymbol (id_clone tv.tv_name) ty_type in
95 96 97
  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
98 99
  f_forall_close_simp vl [] (fn tvm f)

François Bobot's avatar
François Bobot committed
100 101 102 103
let f_type_close fn f =
  let tvs = f_ty_freevars Stv.empty f in
  type_close tvs fn f

104
(* convert a type declaration to a list of lsymbol declarations *)
105
let lsdecl_of_tydecl acc td = match td with
106 107 108 109 110
    | 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
111 112 113 114 115 116 117 118 119 120 121



(* 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
122
  in
123 124 125 126
  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
127 128

(* convert a constant to a functional symbol of type ty_base *)
129
let ls_of_const ty_base =
130
  let ht = Hterm.create 63 in
131
  fun t -> match t.t_node with
132 133
    | Tconst _ ->
        begin try Hterm.find ht t with Not_found ->
134
          let s = "const_" ^ Pp.string_of_wnl Pretty.print_term t in
135
          let ls = create_fsymbol (id_fresh s) [] ty_base in
136 137
          Hterm.add ht t ls;
          ls
138 139 140
        end
    | _ -> assert false

141 142 143 144 145 146
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
147 148 149

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

150
let vs_monomorph ty_base kept vs =
151 152
  if Sty.mem vs.vs_ty kept then vs else
  create_vsymbol (id_clone vs.vs_name) ty_base
153

154 155 156
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
157 158 159
  t_label_copy t (match t.t_node with
    | Tvar v ->
        Mvs.find v vmap
160
    | Tconst _ when Sty.mem (t_type t) kept ->
161
        t
162 163
    | Tconst _ ->
        let ls = ls_of_const ty_base t in
164 165 166 167 168 169 170 171 172 173
        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
174
        let v = vs_monomorph ty_base kept u in
175 176 177 178 179 180
        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
181
        let v = vs_monomorph ty_base kept u in
182
        let f = f_mono (Mvs.add u (t_var v) vmap) f in
183 184
        t_eps (close v f)
    | Fquant _ | Fbinop _ | Fnot _ | Ftrue | Ffalse -> raise (TermExpected t))
185

186 187 188
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
189 190
  f_label_copy f (match f.t_node with
    | Tapp (ps,[t1;t2]) when ls_equal ps ps_equ ->
191
        f_equ (t_mono vmap t1) (t_mono vmap t2)
192
    | Tapp (ps,tl) ->
193 194 195
        f_app (lsmap ps) (List.map (t_mono vmap) tl)
    | Fquant (q,b) ->
        let ul,tl,f1,close = f_open_quant_cb b in
196
        let vl = List.map (vs_monomorph ty_base kept) ul in
197 198 199 200 201 202 203 204 205 206
        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
207
    | Tif (f1,f2,f3) ->
208
        f_if (f_mono vmap f1) (f_mono vmap f2) (f_mono vmap f3)
209
    | Tlet (t,b) ->
210
        let u,f1,close = f_open_bound_cb b in
211
        let v = vs_monomorph ty_base kept u in
212 213
        let f1 = f_mono (Mvs.add u (t_var v) vmap) f1 in
        f_let (t_mono vmap t) (close v f1)
214 215 216
    | Tcase _ ->
        Printer.unsupportedFmla f "no match expressions at this point"
    | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f))
217

218 219
let d_monomorph ty_base kept lsmap d =
  let kept = Sty.add ty_base kept in
220
  let consts = ref Sls.empty in
221 222
  let t_mono = t_monomorph ty_base kept lsmap consts in
  let f_mono = f_monomorph ty_base kept lsmap consts in
223 224 225 226 227 228
  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
229
          | ts, _ when not (Sty.exists (ty_s_any (ts_equal ts)) kept) -> acc
230 231 232 233 234 235
          | _ -> 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
236
            if ls_equal ls ps_equ then ls else lsmap ls
237 238 239 240
          in
          match ld with
          | Some ld ->
              let ul,e = open_ls_defn ld in
241
              let vl = List.map (vs_monomorph ty_base kept) ul in
242 243
              let add acc u v = Mvs.add u (t_var v) acc in
              let vmap = List.fold_left2 add Mvs.empty ul vl in
Andrei Paskevich's avatar
Andrei Paskevich committed
244
              let e = e_fold t_mono f_mono vmap e in
245 246 247 248 249 250
              make_ls_defn ls vl e
          | None ->
              ls, None
        in
        [create_logic_decl (List.map conv ldl)]
    | Dind idl ->
251
        let iconv (pr,f) = pr, f_mono Mvs.empty f in
252 253 254
        let conv (ls,il) = lsmap ls, List.map iconv il in
        [create_ind_decl (List.map conv idl)]
    | Dprop (k,pr,f) ->
255
        [create_prop_decl k pr (f_mono Mvs.empty f)]
256 257 258
  in
  let add ls acc = create_logic_decl [ls,None] :: acc in
  Sls.fold add !consts dl
259 260 261 262 263 264 265 266 267 268 269 270 271

(** 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
272
      Trans.add_tdecls (Sty.fold fold kept' []))