encoding_instantiate.ml 19.8 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
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Stdlib
21 22 23 24 25 26 27 28
open Util
open Ident
open Ty
open Term
open Task
open Theory
open Task
open Decl
29
open Encoding
30

31
let meta_complete = register_meta_excl
32
  "encoding_instantiate : complete" [MTstring]
33

34
exception TooMuchInstantiation of int
35
let max_instantiation = 512 (* 7 ** 3 = 343 *)
36 37 38 39 40 41 42

let () = Exn_printer.register (fun fmt exn ->
  match exn with
    | TooMuchInstantiation i -> Format.fprintf fmt
      "encoding_instantiate : %i instantiation to create, it is limited to %i"
      i max_instantiation
    | _ -> raise exn)
43

44
(* Ce type est utiliser pour indiquer un alpha *)
45
let tv_dumb = create_tvsymbol (id_fresh "instantiate_alpha")
46 47
let ty_dumb = ty_var tv_dumb

48 49 50
(* TODO : transmettre les tags des logiques polymorphe vers les logiques
   instantié. Un tag sur un logique polymorphe doit être un tag sur toute
   la famille de fonctions *)
51

Andrei Paskevich's avatar
Andrei Paskevich committed
52 53 54 55 56
module OHTyl = OrderedHashList(struct
  type t = ty
  let tag = ty_hash
end)

57
module Mtyl = Map.Make(OHTyl)
58
module Htyl = Hashtbl.Make(OHTyl)
59 60

type tenv =
61 62 63
  | Complete (* The transformation keep the polymorphism *)
  | Incomplete (* The environnement when the transformation isn't complete*)

64

65
(* A type is projected on term or type depending
66
   of its color (green part,red part, black part) *)
67
type tty =
68
  | Tyterm of ty
69 70
  | Tyty of ty

71
let print_tty fmt = function
72
  | Tyterm ty -> Format.fprintf fmt "(Tyterm %a)" Pretty.print_ty ty
73 74
  | Tyty ty -> Format.fprintf fmt "(Tyty %a)" Pretty.print_ty ty

75 76
(* It can be backprojected to type, ty_dumb is like a bottom type it
   never appear in final formulas *)
77 78 79 80 81
let reduce_to_type = function
  | Tyty ty -> ty
  | Tyterm _ -> ty_dumb


82 83 84 85 86 87 88 89 90 91 92 93 94 95
let reduce_to_real = function
  | Tyty ty | Tyterm ty -> ty

(* let reduce_to_pos tenv = function *)
(*   | Tyty ty -> ty *)
(*   | Tyterm _ -> match tenv with  *)
(*       | Incomplete -> assert false (\* All is type in this mode *\) *)
(*       | Tenv tenv -> tenv.undeco *)

(* let reduce_to_neg tenv = function *)
(*   | Tyty ty -> ty *)
(*   | Tyterm _ -> match tenv with  *)
(*       | Incomplete -> assert false (\* All is type in this mode *\) *)
(*       | Tenv tenv -> tenv.deco *)
96

97
(* The environnement of the transformation between two decl (* unmutable *) *)
98 99 100
type env = {
  etenv : tenv;
  ekeep : Sty.t;
101
  prop_toremove : ty Mtv.t Mpr.t;
102 103
  eprojty : ty Mty.t;
  edefined_lsymbol : lsymbol Mtyl.t Mls.t;
104
  edefined_tsymbol : tysymbol Mtyl.t Mts.t;
105 106
}

107
type auto_clone = task -> tenv -> Sty.t -> task * env
108

109
(* The environnement of the transformation during
110
   the transformation of a formula *)
111 112 113 114 115
type menv = {
  tenv : tenv;
  keep : Sty.t;
  mutable projty : ty Mty.t;
  mutable defined_lsymbol : lsymbol Mtyl.t Mls.t;
116
  mutable defined_tsymbol : tysymbol Mtyl.t Mts.t;
117 118 119 120 121 122
  mutable undef_lsymbol : Sls.t;
  mutable undef_tsymbol : Sts.t;
}

let print_env fmt menv =
  Format.fprintf fmt "defined_lsymbol (%a)@."
123
    (Pp.print_iter2 Mls.iter Pp.semi Pp.comma Pretty.print_ls
124 125 126 127
       (Pp.print_iter2 Mtyl.iter Pp.semi Pp.arrow
          (Pp.print_list Pp.space Pretty.print_ty)
          Pretty.print_ls)) menv.defined_lsymbol;
  Format.fprintf fmt "defined_tsymbol (%a)@."
128
    (Pp.print_iter2 Mts.iter Pp.semi Pp.comma Pretty.print_ts
129 130
       (Pp.print_iter2 Mtyl.iter Pp.semi Pp.arrow
          (Pp.print_list Pp.space Pretty.print_ty)
131
          Pretty.print_ts)) menv.defined_tsymbol
132

133
type tvar = ty Mtv.t
134

135
let rec projty menv tvar ty =
136 137
  let rec aux ty =
    match ty.ty_node with
138
      | Tyvar _ -> Tyterm ty
139 140 141 142 143
      | Tyapp (ts,tyl) ->
        try
          Tyty (Mty.find ty menv.projty)
        with Not_found ->
          match menv.tenv with
144
            | Incomplete ->
145
              (* In this configuration there is no term representing type,
146
                 all type are a type or are in the black part
147
                 (the or is not a xor)*)
148 149 150 151
              (* let preid = id_clone ts.ts_name in *)
              (* let ts = create_tysymbol preid [] None (\*Some ty*\) in *)
              (* let tty = ty_app ts [] in *)
              let tty = ty in
152 153 154 155 156
              menv.projty <- Mty.add ty tty menv.projty;
              menv.undef_tsymbol <- Sts.add ts menv.undef_tsymbol;
              (*Format.eprintf "projty : ts : %a env : %a@." Pretty.print_ts ts
              print_env menv;*)
              Tyty tty
157
            | Complete ->
158 159
              let tyl = List.map aux tyl in
              let tyl_red = List.map reduce_to_type tyl in
160
              let tys =
161 162 163 164 165 166 167
                try
                  Mtyl.find tyl_red (Mts.find ts menv.defined_tsymbol)
                with Not_found ->
                  let insts = try Mts.find ts menv.defined_tsymbol
                    with Not_found -> Mtyl.empty in
                  let args = List.fold_left (fun acc e ->
                    match e with
168
                      | Tyterm _ -> (create_tvsymbol (id_fresh "a"))::acc
169
                      | Tyty _ -> acc) [] tyl in
170 171
                  let tys = if List.length args = List.length ts.ts_args
                    then ts
172 173
                    else create_tysymbol (id_clone ts.ts_name) args None in
                  let insts = Mtyl.add tyl_red tys insts in
174 175
                  menv.defined_tsymbol <-
                    Mts.add ts insts menv.defined_tsymbol;
176 177
                  menv.undef_tsymbol <- Sts.add tys menv.undef_tsymbol;
                  tys in
178 179
              let args = List.rev (List.fold_left (fun acc e ->
                match e with
180
                  | Tyterm ty -> ty::acc
181
                  | Tyty _ -> acc) [] tyl) in
182 183
              Tyterm (ty_app tys args) in
  let ty = ty_inst tvar ty in
184 185
  aux ty

186 187 188 189 190 191 192 193 194
let projty_real menv tvar ty = reduce_to_real (projty menv tvar ty)

(* let reduce_to_default menv d = function *)
(*   | Tyty ty -> ty *)
(*   | Tyterm ty -> match menv.tenv with *)
(*       | Incomplete -> ty *)
(*       | Complete -> projty menv Mtv.empty d *)


195
let reduce_to_default menv tvar d ty =
196
  match projty menv tvar ty with
197
    | Tyty _ -> (*keep the term unfolded *) ty_inst tvar ty
198 199
    | Tyterm _ -> ty_var d

200 201 202 203 204 205 206 207 208 209 210 211 212 213
(* Weakmemo only on the symbols *)
let clone_lsymbol_memo =
  let clone_lsymbol p =
    let h = Htyl.create 7 in
    fun arg result ->
      let key = (option_apply arg (fun r -> r::arg) result) in
      try
        Htyl.find h key
      with Not_found ->
        let p = create_lsymbol (id_clone p.ls_name) arg result in
        Htyl.add h key p;
        p in
  Wls.memoize 7 clone_lsymbol

214 215 216
let find_logic menv tvar p tyl ret =
  if ls_equal p ps_equ then p else begin
    let inst = ls_app_inst p tyl ret in
217 218 219
     (* Format.eprintf "inst : %a@." *)
     (*   (Pp.print_iter2 Mtv.iter Pp.comma Pp.space Pp.nothing *)
     (*      Pretty.print_ty) inst; *)
220 221
    let inst = Mtv.mapi (reduce_to_default menv tvar) inst in
    let inst_l = Mtv.fold (fun _ v acc -> v::acc) inst [] in
222 223
    (* Format.eprintf "p : %a | arg : %a| tyl = %a | inst_l : %a@." *)
    (*   Pretty.print_ls p *)
224
    (*   (Pp.print_list Pp.comma Pretty.print_ty) p.ls_args *)
225 226 227
    (*   (Pp.print_list Pp.comma Pretty.print_ty) *)
    (*   (List.map (fun t -> (projty_real menv tvar t.t_ty)) tyl) *)
    (*   (Pp.print_list Pp.comma Pretty.print_ty) inst_l; *)
228 229
      try
      let insts = Mls.find p menv.defined_lsymbol in
230
      Mtyl.find inst_l insts
231
    with Not_found ->
232
      let insts =
233 234 235 236
        try
          Mls.find p menv.defined_lsymbol
        with Not_found ->
          Mtyl.empty in
237
      (* proj fold the types previously kept unfold in inst *)
238 239 240 241 242
      let proj ty = reduce_to_real (projty menv Mtv.empty ty) in
      let arg = List.map (ty_inst inst) p.ls_args in
      let arg = List.map proj arg in
      let result = option_map (ty_inst inst) p.ls_value in
      let result = option_map proj result in
243 244 245
      (* Format.eprintf "arg : %a ; result : %a@." *)
      (*   (Pp.print_list Pp.comma Pretty.print_ty) arg *)
      (*   (Pp.print_option Pretty.print_ty) result; *)
246
      let ls = if List.for_all2 ty_equal arg p.ls_args &&
247
          option_eq ty_equal result p.ls_value
248
        then p else clone_lsymbol_memo p arg result in
249 250 251
      let insts = Mtyl.add inst_l ls insts in
      menv.defined_lsymbol <- Mls.add p insts menv.defined_lsymbol;
      menv.undef_lsymbol <- Sls.add ls menv.undef_lsymbol;
252
      (* Format.eprintf "fl : env : %a  p : %a | inst : %a@." *)
253 254 255 256 257 258 259 260 261 262 263 264 265
      (*   print_env menv *)
      (*   Pretty.print_ls p *)
      (*   (Pp.print_list Pp.comma Pretty.print_ty) inst_l; *)
      ls
  end


(* let deco_res menv t ty = *)
(*   match ty with *)
(*     | Tyty _ -> t *)
(*     | Tyterm tyterm -> *)
(*       match menv.tenv with *)
(*         | Incomplete -> assert false *)
266
(*         | Tenv tenv -> fs_app tenv.sort [tyterm;t] tenv.deco *)
267 268 269 270

(* let sort_app tenv ty t = *)
(*   match tenv with *)
(*     | Incomplete -> assert false *)
271
(*     | Tenv tenv -> fs_app tenv.sort [ty;t] tenv.deco    *)
272 273 274


let conv_vs menv tvar vsvar vs =
275 276 277 278
  let ty = projty_real menv tvar vs.vs_ty in
  let vs' = if ty_equal ty vs.vs_ty then vs else
      create_vsymbol (id_clone vs.vs_name) ty in
  Mvs.add vs (t_var vs') vsvar,vs'
279

280
(* The convertion of term and formula *)
281
let rec rewrite_term menv tvar vsvar t =
282 283
  let fnT = rewrite_term menv tvar in
  let fnF = rewrite_fmla menv tvar in
284
  (* Format.eprintf "@[<hov 2>Term : %a =>@\n@?" Pretty.print_term t; *)
285
  let t = match t.t_node with
286 287
    | Tconst _ -> t
    | Tvar x -> Mvs.find x vsvar
288
    | Tapp(p,tl) ->
289
      let tl' = List.map (fnT vsvar) tl in
290
      let p = find_logic menv tvar p tl t.t_ty in
291
      fs_app p tl' (projty_real menv tvar (t_type t))
292 293
    | Tif(f, t1, t2) ->
      t_if (fnF vsvar f) (fnT vsvar t1) (fnT vsvar t2)
294
    | Tlet (t1, b) -> let u,t2,cb = t_open_bound_cb b in
295
      let (vsvar',u) = conv_vs menv tvar vsvar u in
296 297
      let t1 = fnT vsvar t1 in let t2 = fnT vsvar' t2 in
      t_let t1 (cb u t2)
298
    | Tcase _ | Teps _ ->
299
      Printer.unsupportedTerm t
300 301 302
        "Encoding instantiate : I can't encode this term"
    | Fquant _ | Fbinop _ | Fnot _ | Ftrue | Ffalse -> raise (TermExpected t)
  in
303 304 305
  (* Format.eprintf "@[<hov 2>Term : => %a : %a@\n@?" *)
  (*   Pretty.print_term t Pretty.print_ty t.t_ty; *)
  t
306

307
and rewrite_fmla menv tvar vsvar f =
308 309
  let fnT = rewrite_term menv tvar in
  let fnF = rewrite_fmla menv tvar in
310
  (* Format.eprintf "@[<hov 2>Fmla : %a =>@\n@?" Pretty.print_fmla f; *)
311 312
  match f.t_node with
    | Tapp(p, tl) ->
313
      let tl' = List.map (fnT vsvar) tl in
314
      let p = find_logic menv tvar p tl None in
315
      ps_app p tl'
316
    | Fquant(q, b) ->
317
      let vl, tl, f1, cb = f_open_quant_cb b in
318
      let vsvar,vl = map_fold_left (conv_vs menv tvar) vsvar vl in
319 320 321

      let f1 = fnF vsvar f1 in
      (* Ici un trigger qui ne match pas assez de variables
322
         peut être généré *)
323
      let tl = TermTF.tr_map (fnT vsvar) (fnF vsvar) tl in
324
      f_quant q (cb vl tl f1)
325
    | Tlet (t1, b) -> let u,f2,cb = t_open_bound_cb b in
326
      let (vsvar',u) = conv_vs menv tvar vsvar u in
327
      let t1 = fnT vsvar t1 and f2 = fnF vsvar' f2 in
328 329
      (* Format.eprintf "u.vs_ty : %a == t1.t_ty : %a@." *)
      (*    Pretty.print_ty u.vs_ty Pretty.print_ty t1.t_ty; *)
330
      ty_equal_check u.vs_ty (t_type t1);
331
      t_let t1 (cb u f2)
332
    | _ -> TermTF.t_map (fun _ -> assert false) (fnF vsvar) f
333

334
(* Generation of all the possible instantiation of a formula *)
335 336
let gen_tvar env ts =
  let aux tv tvarl =
337
    let gen tvar ty = Mtv.add tv ty tvar in
338
    let tvarl' = List.fold_left (fun acc tvar ->
339 340
      Sty.fold (fun ty acc -> gen tvar ty :: acc) env.ekeep acc) [] tvarl in
    match env.etenv with
341 342 343
      | Incomplete -> tvarl'
      | Complete ->
        let gen acc tvar = (Mtv.add tv (ty_var tv) tvar)::acc in
344
        List.fold_left gen tvarl' tvarl in
345
  Stv.fold aux ts [Mtv.empty]
346 347

(*
348
let ty_args_from_tty =
349 350 351
  List.fold_left (fun acc e ->
    match e with
      | Tyterm _ -> tenv.ty::acc
352
      | Tyty _ -> acc) []
353 354 355

let conv_to_tty env ts tyl proj_ty =
  let ty = ty_app ts tyl in
356
  if Sty.mem ty env.keep
357 358 359 360 361 362 363 364
  then (assert (Mty.mem ty proj_ty); proj_ty)
  else let args = ty_args_from_tty tyl in
*)

let ty_quant =
  let rec add_vs s ty = match ty.ty_node with
    | Tyvar vs -> Stv.add vs s
    | _ -> ty_fold add_vs s ty in
365
  t_ty_fold add_vs Stv.empty
366

367 368 369 370 371 372 373 374 375 376
let add_decl_ud menv task =
  let task = Sts.fold
    (fun ts task -> add_ty_decl task [ts,Tabstract])
    menv.undef_tsymbol task in
  let task = Sls.fold
    (fun ls task -> add_logic_decl task [ls,None])
    menv.undef_lsymbol task in
  task


377
(* The Core of the transformation *)
378
let fold_map task_hd ((env:env),task) =
379
  match task_hd.task_decl.td_node with
380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411
    | Use _ | Clone _ -> env,add_tdecl task task_hd.task_decl
    | Meta(meta,ml) ->
      begin try
        let menv =  {
          tenv = env.etenv;
          keep = env.ekeep;
          projty = env.eprojty;
          defined_lsymbol = env.edefined_lsymbol;
          defined_tsymbol = env.edefined_tsymbol;
          undef_lsymbol = Sls.empty;
          undef_tsymbol = Sts.empty;
        } in
        let map = function
          | MAty ty -> MAty (projty_real menv Mtv.empty ty)
          (* | MAts {ts_name = name; ts_args = []; ts_def = Some ty} -> *)
          (*   MAts (conv_ts tenv ud name ty) *)
          (* | MAts {ts_args = []; ts_def = None} as x -> x *)
          | MAts _ -> raise Exit
          | MAls _ -> raise Exit
          | MApr _ -> raise Exit
          | MAstr _ as s -> s
          | MAint _ as i -> i in
        let arg = (List.map map ml) in
        let task = add_meta (add_decl_ud menv task) meta arg in
        {env with edefined_lsymbol = menv.defined_lsymbol;
          edefined_tsymbol = menv.defined_tsymbol;
          eprojty = menv.projty;
        }, task
      with
        | Printer.UnsupportedType _
        | Exit -> env,add_tdecl task task_hd.task_decl
      end
412 413
    | Decl d -> match d.d_node with
    | Dtype [_,Tabstract] -> (env,task)
414
    (* Nothing here since the type kept are already defined and the other
415
       will be lazily defined *)
416
    | Dtype _ -> Printer.unsupportedDecl
417 418 419 420
        d "encoding_decorate : I can work only on abstract\
            type which are not in recursive bloc."
    | Dlogic l ->
        let fn = function
421 422
          | _, Some _ ->
              Printer.unsupportedDecl
423 424 425 426 427
                d "encoding_decorate : I can't encode definition. \
Perhaps you could use eliminate_definition"
          | _, None -> () in
            (* Noting here since the logics are lazily defined *)
            List.iter fn l; (env,task)
428
    | Dind _ -> Printer.unsupportedDecl
429 430 431 432 433 434
        d "encoding_decorate : I can't work on inductive"
        (* let fn (pr,f) = pr, fnF f in *)
        (* let fn (ps,l) = ps, List.map fn l in *)
        (* [create_ind_decl (List.map fn l)] *)
    | Dprop (k,pr,f) ->
      let tvl = ty_quant f in
435
      assert (k <> Pgoal || Ty.Stv.is_empty tvl);
436 437
      let tvarl = gen_tvar env tvl in
      let tvarl_len = List.length tvarl in
438 439
      if tvarl_len > max_instantiation then
        raise (TooMuchInstantiation tvarl_len);
440 441 442 443 444 445 446 447 448
      let menv =  {
        tenv = env.etenv;
        keep = env.ekeep;
        projty = env.eprojty;
        defined_lsymbol = env.edefined_lsymbol;
        defined_tsymbol = env.edefined_tsymbol;
        undef_lsymbol = Sls.empty;
        undef_tsymbol = Sts.empty;
      } in
449
      let conv_f task tvar =
450 451 452 453 454
        if begin
          try (Mtv.equal ty_equal) tvar (Mpr.find pr env.prop_toremove)
          with Not_found -> false end
        then task
        else
455
        (* Format.eprintf "f0 : %a@. env : %a@." Pretty.print_fmla *)
456
        (*   (t_ty_subst tvar Mvs.empty f) *)
457
        (*   print_env menv; *)
458
        let f = rewrite_fmla menv tvar Mvs.empty f in
459 460
        (* Format.eprintf "f : %a@. env : %a@." Pretty.print_fmla f *)
        (*   print_env menv; *)
461 462
        let pr =
          if tvarl_len = 1 then pr
463
          else create_prsymbol (id_clone pr.pr_name) in
464 465 466 467 468
        (* Format.eprintf "undef ls : %a, ts : %a@." *)
        (*   (Pp.print_iter1 Sls.iter Pp.comma Pretty.print_ls) *)
        (*   menv.undef_lsymbol *)
        (*   (Pp.print_iter1 Sts.iter Pp.comma Pretty.print_ts) *)
        (*   menv.undef_tsymbol; *)
469
        let task = add_decl_ud menv task in
470 471 472 473 474 475 476 477 478 479 480
        let task = add_prop_decl task k pr f in
        task
      in
      {env with edefined_lsymbol = menv.defined_lsymbol;
        edefined_tsymbol = menv.defined_tsymbol;
        eprojty = menv.projty;
      },
      List.fold_left conv_f task tvarl


let monomorphise_goal =
481
  Trans.goal (fun pr f ->
482
    let stv = ty_quant f in
483
    let mty,ltv = Stv.fold (fun tv (mty,ltv) ->
484 485
      let ts = create_tysymbol (id_clone tv.tv_name) [] None in
      Mtv.add tv (ty_app ts []) mty,ts::ltv) stv (Mtv.empty,[]) in
486
    let f = t_ty_subst mty Mvs.empty f in
487 488 489 490 491 492
    let acc = [create_prop_decl Pgoal pr f] in
    let acc = List.fold_left
      (fun acc ts -> (create_ty_decl [ts,Tabstract]) :: acc)
      acc ltv in
    acc)

493

494
(* Some general env creation function *)
François Bobot's avatar
François Bobot committed
495 496
let create_env task tenv keep =
  let projty = Sty.fold (fun ty ty_ty ->
497
    Mty.add ty ty ty_ty)
498
    keep Mty.empty in
François Bobot's avatar
François Bobot committed
499
  let task = Sty.fold (fun ty task ->
500 501 502
    let add_ts task ts = add_ty_decl task [ts,Tabstract] in
    let task = ty_s_fold add_ts task ty in
    task (* the meta is yet here *)) keep task in
François Bobot's avatar
François Bobot committed
503
  task,{
504
    etenv = tenv;
505
    ekeep = keep;
506
    prop_toremove = Mpr.empty;
507 508 509 510 511
    eprojty = projty;
    edefined_lsymbol = Mls.empty;
    edefined_tsymbol = Mts.empty
  }

512
(* This one take use the tag but also all the type which appear in the goal *)
513
let is_ty_mono ~only_mono ty =
514 515 516 517 518 519 520 521
  try
    let rec check () ty = match ty.ty_node with
      | Tyvar _ -> raise Exit
      | Tyapp _ -> ty_fold check () ty in
    check () ty;
    true
  with Exit when not only_mono -> false

522

523
let create_trans_complete kept complete =
524 525 526 527 528
  let task = use_export None builtin_theory in
  let tenv = match complete with
    | None | Some [MAstr "yes"] -> Complete
    | Some [MAstr "no"] ->  Incomplete
    | _ -> failwith "instantiate complete wrong argument" in
529
  let init_task,env = create_env task tenv kept in
530 531
  Trans.fold_map fold_map env init_task

532
let encoding_instantiate =
533 534 535 536
  Trans.compose Libencoding.close_kept
  (Trans.on_tagged_ty meta_kept (fun kept ->
    Trans.on_meta_excl meta_complete (fun complete ->
      create_trans_complete kept complete)))
537

538 539
let () = Hashtbl.replace Encoding.ft_enco_kept "instantiate"
  (const encoding_instantiate)
540 541


542
let create_trans_complete create_env kept complete =
543 544 545 546 547
  let task = use_export None builtin_theory in
  let tenv = match complete with
    | None | Some [MAstr "yes"] -> Complete
    | Some [MAstr "no"] ->  Incomplete
    | _ -> failwith "instantiate complete wrong argument" in
548
  let init_task,env = create_env task tenv kept in
549 550 551
  Trans.fold_map fold_map env init_task

let t create_env =
552
  Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
553
  Trans.on_meta_excl meta_complete (fun complete ->
554
      create_trans_complete create_env kept complete))
555 556 557 558 559 560

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. byte"
End:
*)