encoding_instantiate.ml 19.7 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 266 267 268 269 270 271
      (*   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 *)
(*         | Tenv tenv -> t_app tenv.sort [tyterm;t] tenv.deco *)

(* let sort_app tenv ty t = *)
(*   match tenv with *)
(*     | Incomplete -> assert false *)
(*     | Tenv tenv -> t_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 291
      let p = find_logic menv tvar p tl t.t_ty in
      t_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 303
        "Encoding instantiate : I can't encode this term" in
  (* Format.eprintf "@[<hov 2>Term : => %a : %a@\n@?" *)
  (*   Pretty.print_term t Pretty.print_ty t.t_ty; *)
  t
304

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

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

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

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

let conv_to_tty env ts tyl proj_ty =
  let ty = ty_app ts tyl in
354
  if Sty.mem ty env.keep
355 356 357 358 359 360 361 362
  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
363
  f_ty_fold add_vs Stv.empty
364

365 366 367 368 369 370 371 372 373 374
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


375
(* The Core of the transformation *)
376
let fold_map task_hd ((env:env),task) =
377
  match task_hd.task_decl.td_node with
378 379 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
    | 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
410 411
    | Decl d -> match d.d_node with
    | Dtype [_,Tabstract] -> (env,task)
412
    (* Nothing here since the type kept are already defined and the other
413
       will be lazily defined *)
414
    | Dtype _ -> Printer.unsupportedDecl
415 416 417 418
        d "encoding_decorate : I can work only on abstract\
            type which are not in recursive bloc."
    | Dlogic l ->
        let fn = function
419 420
          | _, Some _ ->
              Printer.unsupportedDecl
421 422 423 424 425
                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)
426
    | Dind _ -> Printer.unsupportedDecl
427 428 429 430 431 432
        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
433
      assert (k <> Pgoal || Ty.Stv.is_empty tvl);
434 435
      let tvarl = gen_tvar env tvl in
      let tvarl_len = List.length tvarl in
436 437
      if tvarl_len > max_instantiation then
        raise (TooMuchInstantiation tvarl_len);
438 439 440 441 442 443 444 445 446
      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
447
      let conv_f task tvar =
448 449 450 451 452
        if begin
          try (Mtv.equal ty_equal) tvar (Mpr.find pr env.prop_toremove)
          with Not_found -> false end
        then task
        else
453
        (* Format.eprintf "f0 : %a@. env : %a@." Pretty.print_fmla *)
454 455
        (*   (f_ty_subst tvar Mvs.empty f) *)
        (*   print_env menv; *)
456
        let f = rewrite_fmla menv tvar Mvs.empty f in
457 458
        (* Format.eprintf "f : %a@. env : %a@." Pretty.print_fmla f *)
        (*   print_env menv; *)
459 460
        let pr =
          if tvarl_len = 1 then pr
461
          else create_prsymbol (id_clone pr.pr_name) in
462 463 464 465 466
        (* 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; *)
467
        let task = add_decl_ud menv task in
468 469 470 471 472 473 474 475 476 477 478
        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 =
479
  Trans.goal (fun pr f ->
480
    let stv = ty_quant f in
481
    let mty,ltv = Stv.fold (fun tv (mty,ltv) ->
482 483 484 485 486 487 488 489 490
      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 = f_ty_subst mty Mvs.empty f in
    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)

491

492
(* Some general env creation function *)
François Bobot's avatar
François Bobot committed
493 494
let create_env task tenv keep =
  let projty = Sty.fold (fun ty ty_ty ->
495
    Mty.add ty ty ty_ty)
496
    keep Mty.empty in
François Bobot's avatar
François Bobot committed
497
  let task = Sty.fold (fun ty task ->
498 499 500
    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
501
  task,{
502
    etenv = tenv;
503
    ekeep = keep;
504
    prop_toremove = Mpr.empty;
505 506 507 508 509
    eprojty = projty;
    edefined_lsymbol = Mls.empty;
    edefined_tsymbol = Mts.empty
  }

510
(* This one take use the tag but also all the type which appear in the goal *)
511
let is_ty_mono ~only_mono ty =
512 513 514 515 516 517 518 519
  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

520

521
let create_trans_complete kept complete =
522 523 524 525 526
  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
527
  let init_task,env = create_env task tenv kept in
528 529
  Trans.fold_map fold_map env init_task

530
let encoding_instantiate =
531 532 533 534
  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)))
535

536 537
let () = Hashtbl.replace Encoding.ft_enco_kept "instantiate"
  (const encoding_instantiate)
538 539


540
let create_trans_complete create_env kept complete =
541 542 543 544 545
  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
546
  let init_task,env = create_env task tenv kept in
547 548 549
  Trans.fold_map fold_map env init_task

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

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