encoding_sort.ml 5.65 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29

open Ident
open Ty
open Term
open Decl
open Theory
open Task

type tenv = {
  specials : tysymbol Hty.t;
  trans_lsymbol : lsymbol Hls.t
}

let init_tenv = {
  specials = Hty.create 17;
  trans_lsymbol = Hls.create 17 }


(* Convert type *)
30 31 32 33 34
let conv_ts tenv undefined name ty =
  let ts =
    try
      Hty.find tenv.specials ty
    with Not_found ->
35
      let ts = create_tysymbol (id_clone name) [] None in
36 37 38 39 40 41
      Hty.add tenv.specials ty ts;
      ts in
  Hts.replace undefined ts ();
  ts


42 43 44
let conv_ty tenv undefined ty =
  match ty.ty_node with
    | Tyapp (_,[]) -> ty
Andrei Paskevich's avatar
Andrei Paskevich committed
45
    | Tyapp (ts,_) ->
46 47
      let ts = conv_ts tenv undefined ts.ts_name ty in
      ty_app ts []
48 49 50 51 52 53
    | _ -> Printer.unsupportedType ty "type variable must be encoded"

(* Convert a variable *)
let conv_vs tenv ud vs =
  let ty = conv_ty tenv ud vs.vs_ty in
  if ty_equal ty vs.vs_ty then vs else
54
  create_vsymbol (id_clone vs.vs_name) ty
55 56 57 58 59

(* Convert a logic symbol to the encoded one *)
let conv_ls tenv ud ls =
  if ls_equal ls ps_equ then ls
  else try Hls.find tenv.trans_lsymbol ls with Not_found ->
60
  let ty_res = Opt.map (conv_ty tenv ud) ls.ls_value in
61 62
  let ty_arg = List.map (conv_ty tenv ud) ls.ls_args in
  let ls' =
63
    if Opt.equal ty_equal ty_res ls.ls_value &&
64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
       List.for_all2 ty_equal ty_arg ls.ls_args then ls
    else create_lsymbol (id_clone ls.ls_name) ty_arg ty_res
  in
  Hls.add tenv.trans_lsymbol ls ls';
  ls'


let rec rewrite_term tenv ud vm t =
  let fnT = rewrite_term tenv ud in
  let fnF = rewrite_fmla tenv ud in
  match t.t_node with
  | Tconst _ -> t
  | Tvar x ->
      Mvs.find x vm
  | Tapp (fs,tl) ->
      let fs = conv_ls tenv ud fs in
      let tl = List.map (fnT vm) tl in
81
      fs_app fs tl (Opt.get fs.ls_value)
82 83 84 85 86 87 88 89
  | Tif (f, t1, t2) ->
      t_if (fnF vm f) (fnT vm t1) (fnT vm t2)
  | Tlet (t1, b) ->
      let u,t2,close = t_open_bound_cb b in
      let u' = conv_vs tenv ud u in
      let t1' = fnT vm t1 in
      let t2' = fnT (Mvs.add u (t_var u') vm) t2 in
      t_let t1' (close u' t2')
90
  | Tcase _ | Teps _ ->
91
      Printer.unsupportedTerm t "unsupported term"
92
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
93 94 95 96

and rewrite_fmla tenv ud vm f =
  let fnT = rewrite_term tenv ud in
  let fnF = rewrite_fmla tenv ud in
97 98
  match f.t_node with
  | Tapp (ps,tl) when ls_equal ps ps_equ ->
99
      ps_app ps (List.map (fnT vm) tl)
100
  | Tapp (ps,tl) ->
101 102
      let ps = conv_ls tenv ud ps in
      let tl = List.map (fnT vm) tl in
103
      ps_app ps tl
104 105
  | Tquant (q,b) ->
      let vl, tl, f1, close = t_open_quant_cb b in
106
      let add m v = let v' = conv_vs tenv ud v in Mvs.add v (t_var v') m, v' in
107
      let vm', vl' = Lists.map_fold_left add vm vl in
108
      let tl' = TermTF.tr_map (fnT vm') (fnF vm') tl in
109
      let f1' = fnF vm' f1 in
110
      t_quant q (close vl' tl' f1')
111
  | Tlet (t1, b) ->
112
      let u,f1,close = t_open_bound_cb b in
113 114 115
      let u' = conv_vs tenv ud u in
      let t1' = fnT vm t1 in
      let f1' = fnF (Mvs.add u (t_var u') vm) f1 in
116
      t_let t1' (close u' f1')
117
  | Tcase _ ->
118
      Printer.unsupportedTerm f "unsupported formula"
119
  | _ -> TermTF.t_map (fnT vm) (fnF vm) f
120

121
let decl_ud ud task =
122
  let add ts () task = add_ty_decl task ts in
123
  Hts.fold add ud task
124

125
let fold tenv taskpre task =
126 127
  let fnT = rewrite_term tenv in
  let fnF = rewrite_fmla tenv in
128 129 130
  match taskpre.task_decl.td_node with
    | Decl d ->
      begin match d.d_node with
131 132 133 134 135 136
        | Dtype { ts_def = Some _ }
        | Dtype { ts_args = _::_ } -> task
        | Dtype ts -> add_ty_decl task ts
        | Ddata _ ->
          Printer.unsupportedDecl d "use eliminate_algebraic"
        | Dparam ls ->
137
          let ud = Hts.create 3 in
138 139 140 141
          let ls = conv_ls tenv ud ls in
          add_param_decl (decl_ud ud task) ls
        | Dlogic _ ->
          Printer.unsupportedDecl d "use eliminate_definition"
142 143 144 145 146
        | Dind _ ->
          Printer.unsupportedDecl d "use eliminate_inductive"
        | Dprop _ ->
          let ud = Hts.create 3 in
          decl_ud ud (add_decl task
147
                        (DeclTF.decl_map (fnT ud Mvs.empty) (fnF ud Mvs.empty) d))
148 149 150 151 152
      end
    | Meta(meta,ml) ->
      begin try
        let ud = Hts.create 3 in
        let map = function
153
          | MAty ty -> MAty (conv_ty tenv ud ty)
154 155
          | MAts {ts_name = name; ts_args = []; ts_def = Some ty} ->
            MAts (conv_ts tenv ud name ty)
François Bobot's avatar
François Bobot committed
156
          | MAts {ts_args = []; ts_def = None} as x -> x
157 158 159 160 161
          | MAts _ -> raise Exit
          | MAls ls -> MAls (conv_ls tenv ud ls)
          | MApr _ -> raise Exit
          | MAstr _ as s -> s
          | MAint _ as i -> i in
162 163
        let arg = List.map map ml in
        add_meta (decl_ud ud task) meta arg
164 165 166 167 168
      with
        | Printer.UnsupportedType _
        | Exit -> add_tdecl task taskpre.task_decl
      end
    | _ -> add_tdecl task taskpre.task_decl
169

Andrei Paskevich's avatar
Andrei Paskevich committed
170
let t =
171
  let tenv = init_tenv in
172
  Trans.fold (fold tenv) None
173

174
let () = Trans.register_transform "encoding_sort" t
175 176
  ~desc:"Remove@ each@ type@ application@ by@ discriminating@ it@ into@ one@ \
         specific@ constant@ type."