libencoding.ml 10.1 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4
5
6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
(*    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
26
27
28
29
30
31
open Theory

let debug = Debug.register_flag "encoding"

(* meta to tag the protected types *)
let meta_kept = register_meta "encoding : kept" [MTty]
32

33
34
35
36
37
38
39
(* sort symbol of the "universal" type *)
let ts_base = create_tysymbol (id_fresh "uni") [] None

(* "universal" sort *)
let ty_base = ty_app ts_base []

(* ts_base declaration *)
40
let d_ts_base = create_ty_decl ts_base
41

42
43
44
45
46
47
48
(* 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 *)
49
let d_ts_type = create_ty_decl ts_type
50
51
52
53
54
55

(* 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)

56
57
58
59
60
61
62
(* 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)

63
64
let ls_int_of_ty = create_fsymbol (id_fresh "int_of_ty") [ty_type] ty_int

65
66
67
68
(** 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
69
    (fun _ -> create_vsymbol (id_fresh "x") ty_type) ts.ts_args
70
71
  in
  let tvars = List.map t_var vars in
72
73
74
  (** type to int *)
  let id = string_of_int (id_hash ts.ts_name) in
  let acc =
75
    let t = fs_app ls tvars ty_type in
76
77
    let f = t_equ (fs_app ls_int_of_ty [t] ty_int) (t_int_const id) in
    let f = t_forall_close vars [[t]] f in
78
79
80
81
82
    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
83
84
  let fmlas = List.rev_map2
    (fun ls_select value ->
85
86
      let t = fs_app ls tvars ty_type in
      let t = fs_app ls_select [t] ty_type in
87
88
      let f = t_equ t value in
      let f = t_forall_close vars [[t]] f in
89
90
91
92
93
94
95
96
      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
97
  let add acc fs = create_param_decl fs :: acc in
98
99
  List.fold_left add props ls_selects

100
101
102
(* convert a type to a term of type ty_type *)
let rec term_of_ty tvmap ty = match ty.ty_node with
  | Tyvar tv ->
103
      Mtv.find tv tvmap
104
  | Tyapp (ts,tl) ->
105
      fs_app (ls_of_ts ts) (List.map (term_of_ty tvmap) tl) ty_type
106

107
(* rewrite a closed formula modulo its free typevars *)
François Bobot's avatar
François Bobot committed
108
let type_close tvs fn f =
109
  let get_vs tv = create_vsymbol (id_clone tv.tv_name) ty_type in
110
111
112
  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
113
  t_forall_close_simp vl [] (fn tvm f)
114

115
let t_type_close fn f =
116
  let tvs = t_ty_freevars Stv.empty f in
François Bobot's avatar
François Bobot committed
117
118
  type_close tvs fn f

119
(* convert a type declaration to a list of lsymbol declarations *)
120
let lsdecl_of_ts ts = create_param_decl (ls_of_ts ts)
121
122

(* convert a type declaration to a list of lsymbol declarations *)
123
124
125
let lsdecl_of_ts_select ts =
  let defs = ls_selects_def_of_ts [] ts in
  create_param_decl (ls_of_ts ts) :: defs
126
127

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

140
141
(* unprotected and unprotecting idents *)

Andrei Paskevich's avatar
Andrei Paskevich committed
142
143
let unprotected_label = Ident.create_label "encoding : unprotected"
let unprotecting_label = Ident.create_label "encoding : unprotecting"
144

145
146
let id_unprotected n = id_fresh ~label:(Slab.singleton unprotected_label) n
let id_unprotecting n = id_fresh ~label:(Slab.singleton unprotecting_label) n
147

148
149
let is_protected_id id = not (Slab.mem unprotected_label id.id_label)
let is_protecting_id id = not (Slab.mem unprotecting_label id.id_label)
150
151
152
153
154
155
156

let is_protected_vs kept vs =
  is_protected_id vs.vs_name && Sty.mem vs.vs_ty kept

let is_protected_ls kept ls =
  is_protected_id ls.ls_name && Sty.mem (of_option ls.ls_value) kept

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

159
let vs_monomorph kept vs =
160
  if is_protected_vs kept vs then vs else
161
  create_vsymbol (id_clone vs.vs_name) ty_base
162

163
164
let rec t_monomorph kept lsmap consts vmap t =
  let t_mono = t_monomorph kept lsmap consts in
165
166
167
  t_label_copy t (match t.t_node with
    | Tvar v ->
        Mvs.find v vmap
168
    | Tconst _ when Sty.mem (t_type t) kept ->
169
        t
170
    | Tconst _ ->
171
        let ls = ls_of_const t in
172
        consts := Sls.add ls !consts;
173
        fs_app ls [] ty_base
174
175
176
177
178
    | Tapp (ps,[t1;t2]) when ls_equal ps ps_equ ->
        t_equ (t_mono vmap t1) (t_mono vmap t2)
    | Tapp (ls,tl) ->
        let ls = lsmap ls in
        t_app ls (List.map (t_mono vmap) tl) ls.ls_value
179
    | Tif (f,t1,t2) ->
180
        t_if (t_mono vmap f) (t_mono vmap t1) (t_mono vmap t2)
181
182
    | Tlet (t1,b) ->
        let u,t2,close = t_open_bound_cb b in
183
        let v = vs_monomorph kept u in
184
185
186
187
188
        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 ->
189
        let u,f,close = t_open_bound_cb b in
190
        let v = vs_monomorph kept u in
191
        let f = t_mono (Mvs.add u (t_var v) vmap) f in
192
        t_eps (close v f)
193
194
    | Tquant (q,b) ->
        let ul,tl,f1,close = t_open_quant_cb b in
195
        let vl = List.map (vs_monomorph kept) ul in
196
197
        let add acc u v = Mvs.add u (t_var v) acc in
        let vmap = List.fold_left2 add vmap ul vl in
198
199
        let tl = tr_map (t_mono vmap) tl in
        t_quant q (close vl tl (t_mono vmap f1))
200
    | Tbinop (op,f1,f2) ->
201
        t_binary op (t_mono vmap f1) (t_mono vmap f2)
202
    | Tnot f1 ->
203
        t_not (t_mono vmap f1)
204
    | Ttrue | Tfalse ->
205
        t)
206

207
let d_monomorph kept lsmap d =
208
  let consts = ref Sls.empty in
209
210
  let kept = Sty.add ty_base kept in
  let t_mono = t_monomorph kept lsmap consts in
211
  let dl = match d.d_node with
212
213
214
215
216
217
218
219
220
    | Dtype { ts_def = Some _ } -> []
    | Dtype ts when not (Sty.exists (ty_s_any (ts_equal ts)) kept) -> []
    | Dtype ts ->
        [create_ty_decl ts]
    | Ddata _ ->
        Printer.unsupportedDecl d "no algebraic types at this point"
    | Dparam ls ->
        let ls = if ls_equal ls ps_equ then ls else lsmap ls in
        [create_param_decl ls]
221
222
    | Dlogic ldl ->
        let conv (ls,ld) =
223
224
225
226
227
228
          let ls = if ls_equal ls ps_equ then ls else lsmap ls in
          let ul,e,close = open_ls_defn_cb ld in
          let vl = List.map (vs_monomorph kept) ul in
          let add acc u v = Mvs.add u (t_var v) acc in
          let vmap = List.fold_left2 add Mvs.empty ul vl in
          close ls vl (t_mono vmap e)
229
230
        in
        [create_logic_decl (List.map conv ldl)]
231
    | Dind (s, idl) ->
232
        let iconv (pr,f) = pr, t_mono Mvs.empty f in
233
        let conv (ls,il) = lsmap ls, List.map iconv il in
234
        [create_ind_decl s (List.map conv idl)]
235
    | Dprop (k,pr,f) ->
236
        [create_prop_decl k pr (t_mono Mvs.empty f)]
237
  in
238
  let add ls acc = create_param_decl ls :: acc in
239
  Sls.fold add !consts dl
240

241
242
243
244
245
246
247
248
249
(* replace type variables in a goal with fresh type constants *)
let monomorphise_goal = Trans.goal (fun pr f ->
  let stv = t_ty_freevars Stv.empty f in
  if Stv.is_empty stv then [create_prop_decl Pgoal pr f] else
  let mty,ltv = Stv.fold (fun tv (mty,ltv) ->
    let ts = create_tysymbol (id_clone tv.tv_name) [] None in
    Mtv.add tv (ty_app ts []) mty, ts::ltv) stv (Mtv.empty,[]) in
  let f = t_ty_subst mty Mvs.empty f in
  List.fold_left
250
    (fun acc ts -> create_ty_decl ts :: acc)
251
252
253
    [create_prop_decl Pgoal pr f] ltv)

(* close by subtype the set of types tagged by meta_kept *)
254
let close_kept =
255
256
257
  Trans.on_tagged_ty meta_kept (fun kept ->
    let rec add acc ty = ty_fold add (Sty.add ty acc) ty in
    let kept' = Sty.fold (Util.flip add) kept kept in
258
259
260
    if kept == kept' then Trans.identity
    else
      let kept' = Sty.diff kept' kept in
261
      let fold ty acc = create_meta meta_kept [MAty ty] :: acc in
262
      Trans.add_tdecls (Sty.fold fold kept' []))
263

264
(* reconstruct a definition of an lsymbol or make a defining axiom *)
265
266
267
268
269
270
let defn_or_axiom ls f =
  match Decl.ls_defn_of_axiom f with
    | Some ld -> [create_logic_decl [ld]]
    | None ->
        let nm = ls.ls_name.id_string ^ "_def" in
        let pr = create_prsymbol (id_derive nm ls.ls_name) in
271
        [create_param_decl ls; create_prop_decl Paxiom pr f]