Commit c8622972 authored by François Bobot's avatar François Bobot

lsinst/kept : add to kept the type in lsinst during select_lsinst instead of during distinction.

currently only for goal and all
parent 71d0df7e
......@@ -234,8 +234,7 @@ let definition_of_env env =
let fold_inst inst lsinst task =
let fold_ty task ty =
let add_ts task ts = add_ty_decl task ([ts,Tabstract]) in
let task = ty_s_fold add_ts task ty in
add_meta task meta_kept [MAty ty] in
ty_s_fold add_ts task ty in
let task = List.fold_left fold_ty task inst in
add_logic_decl task [lsinst,None]
in
......
......@@ -89,6 +89,19 @@ module Env = struct
include Encoding_distinction.Env
(** creation functions *)
(** find type in env *)
let meta_kept_from_env decls env =
let fold_ls _ insts decls =
let fold_inst inst _ decls =
let fold_ty decls ty =
create_meta meta_kept [MAty ty] :: decls in
List.fold_left fold_ty decls inst
in
Mtyl.fold fold_inst insts decls
in
Mls.fold fold_ls env decls
(** Using an lskept *)
let env_from_fold lskept (env,kept) ls tyl tyv =
if Sls.mem ls lskept &&
......@@ -172,14 +185,18 @@ let inst_goal _env =
Trans.compose (inst_nothing _env) $
Trans.tgoal (fun pr f ->
let env = f_app_fold add_mono_instantiation Mls.empty f in
metas_of_env env [create_decl (create_prop_decl Pgoal pr f)])
let decls = [create_decl (create_prop_decl Pgoal pr f)] in
let decls = meta_kept_from_env decls env in
metas_of_env env decls)
(** goal + context *)
let inst_all _env =
Trans.compose (inst_nothing _env) $
Trans.bind (Trans.fold fold_add_instantion Mls.empty)
(fun env -> Trans.add_tdecls (metas_of_env env []))
(fun env ->
let decls = meta_kept_from_env [] env in
Trans.add_tdecls (metas_of_env env decls))
(** register *)
let () = register ft_select_lsinst inst_nothing inst_goal inst_all
......
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