Commit 74b83897 authored by François Bobot's avatar François Bobot

monomorphise goal where removed at some point. Redo it...

parent db16f316
......@@ -73,11 +73,40 @@ let maybe_encoding_enumeration =
then Encoding_enumeration.encoding_enumeration
else identity)
let encoding_smt env = compose maybe_encoding_enumeration
(compose (enco_select env) (compose (enco_kept env) (enco_poly_smt env)))
let encoding_tptp env = compose Encoding_enumeration.encoding_enumeration
(compose (enco_select env) (compose (enco_kept env) (enco_poly_tptp env)))
open Ty
open Term
let ty_all_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
f_ty_fold add_vs Stv.empty
let monomorphise_goal =
Trans.goal (fun pr f ->
let stv = ty_all_quant f in
let mty,ltv = Stv.fold (fun tv (mty,ltv) ->
let ts = create_tysymbol (Ident.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 = [Decl.create_prop_decl Decl.Pgoal pr f] in
let acc = List.fold_left
(fun acc ts -> (Decl.create_ty_decl [ts,Decl.Tabstract]) :: acc)
acc ltv in
acc)
let encoding_smt env =
compose monomorphise_goal
(compose maybe_encoding_enumeration
(compose (enco_select env)
(compose (enco_kept env) (enco_poly_smt env))))
let encoding_tptp env =
compose monomorphise_goal
(compose Encoding_enumeration.encoding_enumeration
(compose (enco_select env)
(compose (enco_kept env) (enco_poly_tptp env))))
let () =
register_env_transform "encoding_smt" encoding_smt;
......
......@@ -292,25 +292,6 @@ Perhaps you could use eliminate_definition"
let task = Ssubst.fold conv_f tvarl task in
{env with edefined_lsymbol = menv.defined_lsymbol}, task
let ty_all_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
f_ty_fold add_vs Stv.empty
let monomorphise_goal =
Trans.goal (fun pr f ->
let stv = ty_all_quant f in
let mty,ltv = Stv.fold (fun tv (mty,ltv) ->
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)
let meta_kept_array = register_meta "encoding : kept_array" [MTtysymbol]
let collect_arrays poly_ts tds =
......
......@@ -385,6 +385,7 @@ Perhaps you could use eliminate_definition"
(* [create_ind_decl (List.map fn l)] *)
| Dprop (k,pr,f) ->
let tvl = ty_quant f in
assert (k <> Pgoal || Ty.Stv.is_empty tvl);
let tvarl = gen_tvar env tvl in
let tvarl_len = List.length tvarl in
let menv = {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment