libencoding.ml 7.87 KB
Newer Older
1
2
3
4
5
6
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
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
72
73
74
75
76
77
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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)

(* test whether a function symbol has ty_type as ls_value *)
let is_ls_of_ts ls = match ls.ls_value with
  | Some { ty_node = Tyapp (ts,_) } when ts_equal ts ts_type -> true
  | _ -> false

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

(* convert a type declaration to a list of lsymbol declarations *)
let lsdecl_of_tydecl tdl =
  let add td acc = 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, _ -> create_logic_decl [ls_of_ts ts, None] :: acc
  in
  List.fold_right add tdl []

(* sort symbol by default (= undeco) *)
let ts_base = create_tysymbol (id_fresh "uni") [] None

(* sort by default (= undeco) *)
let ty_base = ty_app ts_base []

(* ts_base declaration *)
let d_ts_base = create_ty_decl [ts_base, Tabstract]

(* convert a constant to a functional symbol of type ty_base *)
let ls_of_const =
  let ht = Hterm.create 63 in
  let ls_of_t t = match t.t_node with
    | Tconst _ ->
        begin try Hterm.find ht t with Not_found ->
78
79
          let s = "const_" ^ Pp.string_of Pretty.print_term t in
          let ls = create_fsymbol (id_fresh s) [] ty_base in
80
81
          Hterm.add ht t ls;
          ls
82
83
84
85
86
87
88
89
        end
    | _ -> assert false
  in
  fun c -> ls_of_t (t_const c)

(* convert a constant to a term of type ty_base *)
let term_of_const c = t_app (ls_of_const c) [] ty_base

90
91
92
(* convert tysymbols tagged with meta_kept to a set of types *)
let get_kept_types tds =
  let tss = Task.find_tagged_ts Encoding.meta_kept tds Sts.empty in
93
94
95
96
  let add ts acc = match ts.ts_def with
    | Some ty -> Sty.add ty acc
    | None -> Sty.add (ty_app ts []) acc
  in
97
  Sts.fold add tss (Sty.singleton ty_type)
98
99
100
101

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

let vs_monomorph kept vs =
102
103
  if Sty.mem vs.vs_ty kept then vs else
  create_vsymbol (id_clone vs.vs_name) ty_base
104
105
106
107
108
109
110
111
112

let rec t_monomorph kept lsmap consts vmap t =
  let t_mono = t_monomorph kept lsmap consts in
  let f_mono = f_monomorph kept lsmap consts in
  t_label_copy t (match t.t_node with
    | Tbvar _ ->
        assert false
    | Tvar v ->
        Mvs.find v vmap
113
114
    | Tconst _ when Sty.mem t.t_ty kept ->
        t
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
    | Tconst c ->
        let ls = ls_of_const c in
        consts := Sls.add ls !consts;
        t_app ls [] ty_base
    | Tapp (fs,_) when is_ls_of_ts fs ->
        t
    | 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
        let v = vs_monomorph kept u in
        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
        let v = vs_monomorph kept u in
        let f = f_mono (Mvs.add u (t_var v) vmap) f in
        t_eps (close v f))

and f_monomorph kept lsmap consts vmap f =
  let t_mono = t_monomorph kept lsmap consts in
  let f_mono = f_monomorph kept lsmap consts in
  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
        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 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
        let v = vs_monomorph kept u in
        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")

let d_monomorph kept lsmap d =
  let consts = ref Sls.empty in
  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
179
          | ts, _ when not (Sty.exists (ty_s_any (ts_equal ts)) kept) -> acc
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
          | _ -> create_ty_decl [td] :: acc
        in
        List.fold_right add tdl []
    | Dlogic ldl ->
        let conv (ls,ld) =
          let ls =
            if ls_equal ls ps_equ || is_ls_of_ts ls then ls else lsmap ls
          in
          match ld with
          | Some ld ->
              let ul,e = open_ls_defn 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
              let e = match e with
                | Term t -> Term (t_monomorph kept lsmap consts vmap t)
                | Fmla f -> Fmla (f_monomorph kept lsmap consts vmap f)
              in
              make_ls_defn ls vl e
          | None ->
              ls, None
        in
        [create_logic_decl (List.map conv ldl)]
    | Dind idl ->
        let iconv (pr,f) = pr, f_monomorph kept lsmap consts Mvs.empty f in
        let conv (ls,il) = lsmap ls, List.map iconv il in
        [create_ind_decl (List.map conv idl)]
    | Dprop (k,pr,f) ->
        [create_prop_decl k pr (f_monomorph kept lsmap consts Mvs.empty f)]
  in
  let add ls acc = create_logic_decl [ls,None] :: acc in
  Sls.fold add !consts dl