* both living in the same context and metasenv *)
let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
let module RT = RefinementTool in
* both living in the same context and metasenv *)
let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg =
let module RT = RefinementTool in
let c1_ty,univ = CicTypeChecker.type_of_aux' metasenv context c1 univ in
let c2_ty,univ = CicTypeChecker.type_of_aux' metasenv context c2 univ in
let rec mk_implicits = function
let c1_ty,univ = CicTypeChecker.type_of_aux' metasenv context c1 univ in
let c2_ty,univ = CicTypeChecker.type_of_aux' metasenv context c2 univ in
let rec mk_implicits = function
List.sort
(fun (i,ctx1,ty1) (j,ctx1,ty1) ->
try List.assoc i meta2no - List.assoc j meta2no
List.sort
(fun (i,ctx1,ty1) (j,ctx1,ty1) ->
try List.assoc i meta2no - List.assoc j meta2no
let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
debug_print (lazy("SUBST: "^CicMetaSubst.ppsubst body_metasenv subst));
let term = CicMetaSubst.apply_subst subst term in
let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
debug_print (lazy("SUBST: "^CicMetaSubst.ppsubst body_metasenv subst));
let term = CicMetaSubst.apply_subst subst term in
debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
let term, ty, metasenv, ugraph =
CicRefine.type_of_aux' metasenv context term ugraph
debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
let term, ty, metasenv, ugraph =
CicRefine.type_of_aux' metasenv context term ugraph
split_metasenv metasenv (spline_len + List.length context)
in
let term = purge_unused_lambdas lambdas_metasenv term in
split_metasenv metasenv (spline_len + List.length context)
in
let term = purge_unused_lambdas lambdas_metasenv term in
debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
term, metasenv, ugraph
debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
term, metasenv, ugraph
(* given a new coercion uri from src to tgt returns
* a list of (new coercion uri, coercion obj, universe graph)
*)
(* given a new coercion uri from src to tgt returns
* a list of (new coercion uri, coercion obj, universe graph)
*)
(* check if the coercion already exists *)
let coercions = CoercDb.to_list () in
let todo_list = get_closure_coercions src tgt uri coercions in
(* check if the coercion already exists *)
let coercions = CoercDb.to_list () in
let todo_list = get_closure_coercions src tgt uri coercions in