eliminate_algebraic.ml 20.3 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10
(*                                                                  *)
(*  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

open Ident
open Ty
open Term
open Decl
16
open Theory
17 18
open Task

19 20
(* a type constructor generates an infinite type if either it is tagged by
   meta_infinite or one of its "material" arguments is an infinite type *)
21

22
let meta_infinite = register_meta "infinite_type" [MTtysymbol]
23 24
  ~desc:"Specify@ that@ the@ given@ type@ has@ always@ an@ infinite@ \
         cardinality."
Andrei Paskevich's avatar
Andrei Paskevich committed
25

26
let meta_material = register_meta "material_type_arg" [MTtysymbol;MTint]
27 28
  ~desc:"If@ the@ given@ type@ argument@ is@ instantiated@ by@ an@ infinite@ \
         type@ then@ the@ associated@ type@ constructor@ is@ infinite"
29

30 31
let get_material_args matl =
  let add_arg acc = function
32
    | [MAts ts; MAint i] ->
33 34 35 36 37
        let acc, mat = try acc, Mts.find ts acc with Not_found ->
          let mat = Array.make (List.length ts.ts_args) false in
          Mts.add ts mat acc, mat in
        Array.set mat i true;
        acc
38 39
    | _ -> assert false
  in
40 41 42 43 44 45 46 47 48 49
  Mts.map Array.to_list (List.fold_left add_arg Mts.empty matl)

let is_infinite_ty inf_ts ma_map =
  let rec inf_ty ty = match ty.ty_node with
    | Tyapp (ts,_) when Mts.mem ts inf_ts -> true
    | Tyapp (ts,_) when not (Mts.mem ts ma_map) -> false
    | Tyapp (ts,l) ->
        let mat = Mts.find ts ma_map in
        List.exists2 (fun mat ty -> mat && inf_ty ty) mat l
    | _ -> false (* FIXME? can we have non-ground types here? *)
50
  in
51
  inf_ty
52

53 54
(** Compile match patterns *)

55
let rec rewriteT t = match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
56
  | Tcase (t,bl) ->
57
      let t = rewriteT t in
58 59 60
      let mk_b b = let p,t = t_open_branch b in [p], rewriteT t in
      let mk_case = t_case_close and mk_let = t_let_close_simp in
      Pattern.compile_bare ~mk_case ~mk_let [t] (List.map mk_b bl)
61
  | _ -> t_map rewriteT t
62

63
let compile_match = Trans.decl (fun d -> [decl_map rewriteT d]) None
64 65 66

(** Eliminate algebraic types and match statements *)

67 68 69
type state = {
  mt_map : lsymbol Mts.t;       (* from type symbols to selector functions *)
  pj_map : lsymbol list Mls.t;  (* from constructors to projections *)
70
  tp_map : decl Mid.t;          (* skipped tuple symbols *)
71 72
  inf_ts : Sts.t;               (* infinite types *)
  ma_map : bool list Mts.t;     (* material type arguments *)
73 74 75
  keep_t : bool;                (* keep algebraic type definitions *)
  keep_e : bool;                (* keep monomorphic enumeration types *)
  keep_r : bool;                (* keep non-recursive records *)
76
  no_ind : bool;                (* do not generate indexing funcitons *)
77 78
}

79
let empty_state = {
80 81
  mt_map = Mts.empty;
  pj_map = Mls.empty;
82
  tp_map = Mid.empty;
83 84
  inf_ts = Sts.add ts_real (Sts.singleton ts_int);
  ma_map = Mts.empty;
85 86 87
  keep_t = false;
  keep_e = false;
  keep_r = false;
88
  no_ind = false;
89 90
}

Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
91 92
let uncompiled = "eliminate_algebraic: compile_match required"

93
let rec rewriteT kn state t = match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
94
  | Tcase (t1,bl) ->
95
      let t1 = rewriteT kn state t1 in
96
      let mk_br (w,m) br =
Andrei Paskevich's avatar
Andrei Paskevich committed
97
        let (p,e) = t_open_branch br in
98
        let e = rewriteT kn state e in
Andrei Paskevich's avatar
Andrei Paskevich committed
99 100
        match p with
        | { pat_node = Papp (cs,pl) } ->
101
            let add_var e p pj = match p.pat_node with
102
              | Pvar v -> t_let_close_simp v (fs_app pj [t1] v.vs_ty) e
103
              | _ -> Printer.unsupportedTerm t uncompiled
104 105 106 107
            in
            let pjl = Mls.find cs state.pj_map in
            let e = List.fold_left2 add_var e pl pjl in
            w, Mls.add cs e m
Andrei Paskevich's avatar
Andrei Paskevich committed
108
        | { pat_node = Pwild } ->
109
            Some e, m
110
        | _ -> Printer.unsupportedTerm t uncompiled
111 112
      in
      let w,m = List.fold_left mk_br (None,Mls.empty) bl in
113
      let find (cs,_) = try Mls.find cs m with Not_found -> Opt.get w in
114 115
      let ts = match t1.t_ty with
        | Some { ty_node = Tyapp (ts,_) } -> ts
116
        | _ -> Printer.unsupportedTerm t uncompiled
117
      in
118 119
      begin match List.map find (find_constructors kn ts) with
        | [t] -> t
120
        | tl  -> t_app (Mts.find ts state.mt_map) (t1::tl) t.t_ty
121 122
      end
  | _ ->
123
      TermTF.t_map (rewriteT kn state) (rewriteF kn state Svs.empty true) t
124

125 126
and rewriteF kn state av sign f = match f.t_node with
  | Tcase (t1,bl) ->
127
      let t1 = rewriteT kn state t1 in
128
      let av' = Mvs.set_diff av (t_vars t1) in
129
      let mk_br (w,m) br =
130
        let (p,e) = t_open_branch br in
131
        let e = rewriteF kn state av' sign e in
Andrei Paskevich's avatar
Andrei Paskevich committed
132 133
        match p with
        | { pat_node = Papp (cs,pl) } ->
134 135
            let get_var p = match p.pat_node with
              | Pvar v -> v
136
              | _ -> Printer.unsupportedTerm f uncompiled
137
            in
138
            w, Mls.add cs (List.map get_var pl, e) m
Andrei Paskevich's avatar
Andrei Paskevich committed
139
        | { pat_node = Pwild } ->
140
            Some e, m
141
        | _ -> Printer.unsupportedTerm f uncompiled
142 143
      in
      let w,m = List.fold_left mk_br (None,Mls.empty) bl in
144
      let find (cs,_) =
145 146
        let vl,e = try Mls.find cs m with Not_found ->
          let var = create_vsymbol (id_fresh "w") in
147
          let get_var pj = var (t_type (t_app_infer pj [t1])) in
148
          List.map get_var (Mls.find cs state.pj_map), Opt.get w
149
        in
150
        let hd = t_app cs (List.map t_var vl) t1.t_ty in
151 152
        match t1.t_node with
        | Tvar v when Svs.mem v av ->
153
            let hd = t_let_close_simp v hd e in if sign
154 155
            then t_forall_close_simp vl [] hd
            else t_exists_close_simp vl [] hd
156
        | _ ->
157 158 159
            let hd = t_equ t1 hd in if sign
            then t_forall_close_simp vl [] (t_implies_simp hd e)
            else t_exists_close_simp vl [] (t_and_simp     hd e)
160
      in
161 162
      let ts = match t1.t_ty with
        | Some { ty_node = Tyapp (ts,_) } -> ts
163
        | _ -> Printer.unsupportedTerm f uncompiled
164
      in
165
      let op = if sign then t_and_simp else t_or_simp in
166
      Lists.map_join_left find op (find_constructors kn ts)
167 168
  | Tquant (q, bf) when (q = Tforall && sign) || (q = Texists && not sign) ->
      let vl, tr, f1, close = t_open_quant_cb bf in
169
      let tr = TermTF.tr_map (rewriteT kn state)
170
                      (rewriteF kn state Svs.empty sign) tr in
171
      let av = List.fold_left (fun s v -> Svs.add v s) av vl in
172
      let f1 = rewriteF kn state av sign f1 in
173 174
      t_quant_simp q (close vl tr f1)
  | Tbinop (o, _, _) when (o = Tand && sign) || (o = Tor && not sign) ->
175
      TermTF.t_map_sign (Util.const (rewriteT kn state))
176
        (rewriteF kn state av) sign f
177
  | Tlet (t1, _) ->
178
      let av = Mvs.set_diff av (t_vars t1) in
179
      TermTF.t_map_sign (Util.const (rewriteT kn state))
180
        (rewriteF kn state av) sign f
181
  | _ ->
182
      TermTF.t_map_sign (Util.const (rewriteT kn state))
183
        (rewriteF kn state Svs.empty) sign f
184

185
let add_selector (state,task) ts ty csl =
186
  (* declare the selector function *)
187
  let mt_id = id_derive ("match_" ^ ts.ts_name.id_string) ts.ts_name in
188
  let mt_ty = ty_var (create_tvsymbol (id_fresh "a")) in
189
  let mt_al = ty :: List.rev_map (fun _ -> mt_ty) csl in
190 191
  let mt_ls = create_fsymbol mt_id mt_al mt_ty in
  let mtmap = Mts.add ts mt_ls state.mt_map in
192
  let task  = add_param_decl task mt_ls in
193 194 195 196
  (* define the selector function *)
  let mt_vs _ = create_vsymbol (id_fresh "z") mt_ty in
  let mt_vl = List.rev_map mt_vs csl in
  let mt_tl = List.rev_map t_var mt_vl in
197
  let mt_add tsk (cs,_) t =
198
    let id = mt_ls.ls_name.id_string ^ "_" ^ cs.ls_name.id_string in
199
    let pr = create_prsymbol (id_derive id cs.ls_name) in
200
    let vl = List.rev_map (create_vsymbol (id_fresh "u")) cs.ls_args in
201
    let hd = fs_app cs (List.rev_map t_var vl) (Opt.get cs.ls_value) in
202
    let hd = fs_app mt_ls (hd::mt_tl) mt_ty in
203
    let vl = List.rev_append mt_vl (List.rev vl) in
204
    let ax = t_forall_close vl [] (t_equ hd t) in
205
    add_prop_decl tsk Paxiom pr ax
206 207
  in
  let task = List.fold_left2 mt_add task csl mt_tl in
208 209
  { state with mt_map = mtmap }, task

210 211 212
let add_selector acc ts ty = function
  | [_] -> acc
  | csl -> add_selector acc ts ty csl
213

214 215 216 217
let add_indexer (state,task) ts ty csl =
  (* declare the indexer function *)
  let mt_id = id_derive ("index_" ^ ts.ts_name.id_string) ts.ts_name in
  let mt_ls = create_fsymbol mt_id [ty] ty_int in
218
  let task  = add_param_decl task mt_ls in
219 220
  (* define the indexer function *)
  let index = ref (-1) in
221
  let mt_add tsk (cs,_) =
222 223 224 225
    incr index;
    let id = mt_ls.ls_name.id_string ^ "_" ^ cs.ls_name.id_string in
    let pr = create_prsymbol (id_derive id cs.ls_name) in
    let vl = List.rev_map (create_vsymbol (id_fresh "u")) cs.ls_args in
226
    let hd = fs_app cs (List.rev_map t_var vl) (Opt.get cs.ls_value) in
Andrei Paskevich's avatar
Andrei Paskevich committed
227
    let ax = t_equ (fs_app mt_ls [hd] ty_int) (t_nat_const !index) in
228
    let ax = t_forall_close (List.rev vl) [[hd]] ax in
229
    add_prop_decl tsk Paxiom pr ax
230 231 232 233
  in
  let task = List.fold_left mt_add task csl in
  state, task

234
let add_discriminator (state,task) ts ty csl =
235
  let d_add (c1,_) task (c2,_) =
236 237 238 239
    let id = c1.ls_name.id_string ^ "_" ^ c2.ls_name.id_string in
    let pr = create_prsymbol (id_derive id ts.ts_name) in
    let ul = List.rev_map (create_vsymbol (id_fresh "u")) c1.ls_args in
    let vl = List.rev_map (create_vsymbol (id_fresh "v")) c2.ls_args in
240 241
    let t1 = fs_app c1 (List.rev_map t_var ul) ty in
    let t2 = fs_app c2 (List.rev_map t_var vl) ty in
242 243 244
    let ax = t_neq t1 t2 in
    let ax = t_forall_close (List.rev vl) [[t2]] ax in
    let ax = t_forall_close (List.rev ul) [[t1]] ax in
245
    add_prop_decl task Paxiom pr ax
246
  in
247 248
  let rec dl_add task = function
    | c :: cl -> dl_add (List.fold_left (d_add c) task cl) cl
249 250 251 252
    | _ -> task
  in
  state, dl_add task csl

253 254
let add_indexer acc ts ty = function
  | [_] -> acc
255
  | _ when (fst acc).keep_t -> acc
256
  | csl when not ((fst acc).no_ind) -> add_indexer acc ts ty csl
257 258
  | csl when List.length csl <= 16 -> add_discriminator acc ts ty csl
  | _ -> acc
259

260 261 262
let meta_proj =
  (* projection symbol, constructor symbol, position, defining axiom *)
  register_meta "algtype projection" [MTlsymbol;MTlsymbol;MTint;MTprsymbol]
Andrei Paskevich's avatar
Andrei Paskevich committed
263
    ~desc:"Specify@ which@ projection@ symbol@ is@ used@ for@ the@ \
264
           given@ constructor@ at@ the@ specified@ position.@ \
Andrei Paskevich's avatar
Andrei Paskevich committed
265
           For@ internal@ use."
266

267
let add_projections (state,task) _ts _ty csl =
268
  (* declare and define the projection functions *)
269
  let pj_add (m,tsk) (cs,pl) =
270
    let id = cs.ls_name.id_string ^ "_proj_" in
271
    let vl = List.rev_map (create_vsymbol (id_fresh "u")) cs.ls_args in
272
    let tl = List.rev_map t_var vl in
273
    let hd = fs_app cs tl (Opt.get cs.ls_value) in
274
    let c = ref 0 in
275 276 277 278 279 280
    let add (pjl,tsk) t pj =
      let ls = incr c; match pj with
        | Some pj -> pj
        | None ->
            let cn = string_of_int !c in
            let id = id_derive (id ^ cn) cs.ls_name in
281
            create_lsymbol id [Opt.get cs.ls_value] t.t_ty
282
      in
283
      let tsk = add_param_decl tsk ls in
284
      let id = id_derive (ls.ls_name.id_string ^ "_def") ls.ls_name in
285
      let pr = create_prsymbol id in
286
      let hh = t_app ls [hd] t.t_ty in
287
      let ax = t_forall_close (List.rev vl) [] (t_equ hh t) in
288 289
      let mal = [MAls ls; MAls cs; MAint (!c - 1); MApr pr] in
      let tsk = add_prop_decl tsk Paxiom pr ax in
Andrei Paskevich's avatar
Andrei Paskevich committed
290 291
      let tsk = if state.keep_t then add_meta tsk meta_proj mal else tsk in
      ls::pjl, tsk
292
    in
293
    let pjl,tsk = List.fold_left2 add ([],tsk) tl pl in
294
    Mls.add cs (List.rev pjl) m, tsk
295 296
  in
  let pjmap, task = List.fold_left pj_add (state.pj_map, task) csl in
297 298
  { state with pj_map = pjmap }, task

299
let add_inversion (state,task) ts ty csl =
300
  if state.keep_t then state, task else
301
  (* add the inversion axiom *)
302
  let ax_id = ts.ts_name.id_string ^ "_inversion" in
303
  let ax_pr = create_prsymbol (id_derive ax_id ts.ts_name) in
304
  let ax_vs = create_vsymbol (id_fresh "u") ty in
305
  let ax_hd = t_var ax_vs in
306
  let mk_cs (cs,_) =
307
    let pjl = Mls.find cs state.pj_map in
308
    let app pj = t_app_infer pj [ax_hd] in
309
    t_equ ax_hd (fs_app cs (List.map app pjl) ty) in
310
  let ax_f = Lists.map_join_left mk_cs t_or csl in
311
  let ax_f = t_forall_close [ax_vs] [] ax_f in
312
  state, add_prop_decl task Paxiom ax_pr ax_f
313

314
let add_type (state,task) (ts,csl) =
315
  (* declare constructors as abstract functions *)
316
  let cs_add tsk (cs,_) = add_param_decl tsk cs in
317 318
  let task =
    if state.keep_t then task else List.fold_left cs_add task csl in
319
  (* add selector, projections, and inversion axiom *)
320 321
  let ty = ty_app ts (List.map ty_var ts.ts_args) in
  let state,task = add_selector (state,task) ts ty csl in
322
  let state,task = add_indexer (state,task) ts ty csl in
323 324
  let state,task = add_projections (state,task) ts ty csl in
  let state,task = add_inversion (state,task) ts ty csl in
325
  state, task
326

327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353
let add_tags mts (state,task) (ts,csl) =
  let rec mat_ts sts ts csl =
    let sts = Sts.add ts sts in
    let add s (ls,_) = List.fold_left (mat_ty sts) s ls.ls_args in
    let stv = List.fold_left add Stv.empty csl in
    List.map (fun v -> Stv.mem v stv) ts.ts_args
  and mat_ty sts stv ty = match ty.ty_node with
    | Tyvar tv -> Stv.add tv stv
    | Tyapp (ts,tl) ->
        if Sts.mem ts sts then raise Exit; (* infinite type *)
        let matl = try Mts.find ts state.ma_map with
          Not_found -> mat_ts sts ts (Mts.find_def [] ts mts) in
        let add s mat ty = if mat then mat_ty sts s ty else s in
        List.fold_left2 add stv matl tl
  in try
    let matl = mat_ts state.inf_ts ts csl in
    let state = { state with ma_map = Mts.add ts matl state.ma_map } in
    let c = ref (-1) in
    let add_material task m =
      incr c;
      if m then add_meta task meta_material [MAts ts; MAint !c] else task
    in
    state, List.fold_left add_material task matl
  with Exit ->
    let state = { state with inf_ts = Sts.add ts state.inf_ts } in
    state, add_meta task meta_infinite [MAts ts]

354
let comp t (state,task) = match t.task_decl.td_node with
355
  | Decl { d_node = Ddata dl } ->
356 357
      (* add type declarations *)
      let conv (cs,pjl) = cs, List.map (fun _ -> None) pjl in
358 359 360 361
      let conv (ts,csl) = ts, List.map conv csl in
      let task = if state.keep_t
        then add_data_decl task (List.map conv dl)
        else List.fold_left (fun t (ts,_) -> add_ty_decl t ts) task dl
362
      in
363
      (* add needed functions and axioms *)
364 365 366 367 368 369
      let state, task = List.fold_left add_type (state,task) dl in
      (* add the tags for infitite types and material arguments *)
      let mts = List.fold_right (fun (t,l) -> Mts.add t l) dl Mts.empty in
      let state, task = List.fold_left (add_tags mts) (state,task) dl in
      (* return the updated state and task *)
      state, task
370
  | Decl d ->
371
      let fnT = rewriteT t.task_known state in
372
      let fnF = rewriteF t.task_known state Svs.empty true in
373
      state, add_decl task (DeclTF.decl_map fnT fnF d)
374 375 376 377 378 379 380 381 382
  | Meta (m, [MAts ts]) when meta_equal m meta_infinite ->
      let state = { state with inf_ts = Sts.add ts state.inf_ts } in
      state, add_tdecl task t.task_decl
  | Meta (m, [MAts ts; MAint i]) when meta_equal m meta_material ->
      let ma = try Array.of_list (Mts.find ts state.ma_map) with
        | Not_found -> Array.make (List.length ts.ts_args) false in
      let ml = Array.set ma i true; Array.to_list ma in
      let state = { state with ma_map = Mts.add ts ml state.ma_map } in
      state, add_tdecl task t.task_decl
383 384
  | _ ->
      state, add_tdecl task t.task_decl
385

386
let comp t (state,task) = match t.task_decl.td_node with
387
  | Decl ({ d_node = Ddata dl } as d) ->
388 389 390 391
      (* are we going to keep this type? *)
      let old_keep_t = state.keep_t in
      let state = match dl with
        | _ when state.keep_t -> state
392
        | [ts, [_]]
393 394
          when state.keep_r && not (Sid.mem ts.ts_name d.d_syms) ->
            { state with keep_t = true }
395
        | [{ ts_args = [] }, csl]
396 397 398 399 400 401 402 403 404 405
          when state.keep_e && List.for_all (fun (_,l) -> l = []) csl ->
            { state with keep_t = true }
        | _ -> state
      in
      let state,task = comp t (state,task) in
      { state with keep_t = old_keep_t }, task
  | _ ->
      comp t (state,task)

let comp t (state,task) = match t.task_decl.td_node with
406
  | Decl ({ d_node = Ddata [ts,_] } as d) when is_ts_tuple ts ->
407
      let tp_map = Mid.add ts.ts_name d state.tp_map in
408 409 410
      { state with tp_map = tp_map }, task
  | Decl d ->
      let rstate,rtask = ref state, ref task in
411
      let add _ d () =
412
        let t = Opt.get (add_decl None d) in
413
        let state,task = comp t (!rstate,!rtask) in
414 415 416 417 418 419 420
        rstate := state ; rtask := task ; None
      in
      let tp_map = Mid.diff add state.tp_map d.d_syms in
      comp t ({ !rstate with tp_map = tp_map }, !rtask)
  | _ ->
      comp t (state,task)

421 422 423 424 425 426 427
let init_task =
  let init = Task.add_meta None meta_infinite [MAts ts_int] in
  let init = Task.add_meta init meta_infinite [MAts ts_real] in
  init

let eliminate_match =
  Trans.compose compile_match (Trans.fold_map comp empty_state init_task)
428

429
let meta_elim = register_meta "eliminate_algebraic" [MTstring]
Andrei Paskevich's avatar
Andrei Paskevich committed
430
  ~desc:"@[<hov 2>Configure the 'eliminate_algebraic' transformation:@\n\
431 432 433
    \"keep_types\" : @[keep algebraic type definitions@]@\n\
    \"keep_enums\" : @[keep monomorphic enumeration types@]@\n\
    \"keep_recs\"  : @[keep non-recursive records@]@\n\
434
    \"no_index\"   : @[do not generate indexing functions@]@]"
435

436 437 438 439 440 441 442
let eliminate_algebraic = Trans.compose compile_match
  (Trans.on_meta meta_elim (fun ml ->
    let st = empty_state in
    let check st = function
      | [MAstr "keep_types"] -> { st with keep_t = true }
      | [MAstr "keep_enums"] -> { st with keep_e = true }
      | [MAstr "keep_recs"]  -> { st with keep_r = true }
443
      | [MAstr "no_index"]   -> { st with no_ind = true }
444 445 446
      | _ -> raise (Invalid_argument "meta eliminate_algebraic")
    in
    let st = List.fold_left check st ml in
447
    Trans.fold_map comp st init_task))
448

449 450 451
(** Eliminate user-supplied projection functions *)

let elim d = match d.d_node with
452
  | Ddata dl ->
453 454
      (* add type declarations *)
      let conv (cs,pjl) = cs, List.map (fun _ -> None) pjl in
455 456
      let conv (ts,csl) = ts, List.map conv csl in
      let td = create_data_decl (List.map conv dl) in
457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472
      (* add projection definitions *)
      let add vs csl acc pj =
        let mk_b (cs,pjl) =
          let mk_v = create_vsymbol (id_fresh "x") in
          let vl = List.map mk_v cs.ls_args in
          let p = pat_app cs (List.map pat_var vl) vs.vs_ty in
          let find acc v = function
            | Some ls when ls_equal ls pj -> t_var v
            | _ -> acc in
          let t = List.fold_left2 find t_true vl pjl in
          t_close_branch p t in
        let bl = List.map mk_b csl in
        let f = t_case (t_var vs) bl in
        let def = make_ls_defn pj [vs] f in
        create_logic_decl [def] :: acc
      in
473
      let add acc (_,csl) =
474
        let (cs,pjl) = List.hd csl in
475
        let ty = Opt.get cs.ls_value in
476 477 478 479 480 481 482 483 484
        let vs = create_vsymbol (id_fresh "v") ty in
        let get l = function Some p -> p::l | _ -> l in
        let pjl = List.fold_left get [] pjl in
        List.fold_left (add vs csl) acc pjl
      in
      td :: List.rev (List.fold_left add [] dl)
  | _ -> [d]

let eliminate_projections = Trans.decl elim None
485 486

let () =
487
  Trans.register_transform "compile_match" compile_match
Andrei Paskevich's avatar
Andrei Paskevich committed
488
    ~desc:"Transform@ pattern-matching@ with@ nested@ patterns@ \
489
      into@ nested@ pattern-matching@ with@ flat@ patterns.";
490
  Trans.register_transform "eliminate_match" eliminate_match
Andrei Paskevich's avatar
Andrei Paskevich committed
491
    ~desc:"Eliminate@ all@ pattern-matching@ expressions.";
492
  Trans.register_transform "eliminate_algebraic" eliminate_algebraic
493
    ~desc:"Replace@ algebraic@ data@ types@ by@ first-order@ definitions.";
494
  Trans.register_transform "eliminate_projections" eliminate_projections
Andrei Paskevich's avatar
Andrei Paskevich committed
495
    ~desc:"Define@ algebraic@ projection@ symbols@ separately."
496 497 498 499 500 501 502 503 504 505 506 507 508 509


(** conditional transformations, only applied when polymorphic types occur *)

let eliminate_algebraic_if_poly =
  Trans.on_meta Detect_polymorphism.meta_monomorphic_types_only
    (function
    | [] -> eliminate_algebraic
    | _ -> Trans.identity)

let () =
  Trans.register_transform "eliminate_algebraic_if_poly"
    eliminate_algebraic_if_poly
    ~desc:"Same@ as@ eliminate_algebraic@ but@ only@ if@ polymorphism@ appear."