+ let purge_unused_lambdas metasenv t =
+ let rec aux = function
+ | Cic.Lambda (_, Cic.Meta (i,_), t) when
+ List.exists (fun (j,_,_) -> j = i) metasenv ->
+ aux (CicSubstitution.subst (Cic.Rel ~-100) t)
+ | Cic.Lambda (name, s, t) ->
+ Cic.Lambda (name, s, aux t)
+ | t -> t
+ in
+ aux t
+ in
+ debug_print (lazy ("\nCOMPOSING"));
+ debug_print (lazy (" c1= "^CicPp.ppterm c1 ^" : "^ CicPp.ppterm c1_ty));
+ debug_print (lazy (" c2= "^CicPp.ppterm c2 ^" : "^ CicPp.ppterm c2_ty));
+ let saturations_for_c1 = count_saturations_needed 0 c1_ty in
+ let saturations_for_c2 = count_saturations_needed 0 c2_ty in
+ let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in
+ let spline_len = saturations_for_c1 + saturations_for_c2 in
+ let c = mk_lambda_spline c spline_len in
+ (* debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c)); *)
+ let c, univ =
+ match rt.RT.type_of_aux' [] [] c univ with
+ | RT.Success (term, ty, metasenv, ugraph) ->
+ debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term));
+ let metasenv = order_metasenv metasenv in
+ debug_print(lazy("ORDERED MENV: "^rt.RT.ppmetasenv [] metasenv));
+ let body_metasenv, lambdas_metasenv =
+ split_metasenv metasenv spline_len
+ in
+ debug_print(lazy("B_MENV: "^rt.RT.ppmetasenv [] body_metasenv));
+ debug_print(lazy("L_MENV: "^rt.RT.ppmetasenv [] lambdas_metasenv));
+ let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
+ debug_print (lazy("SUBST: "^rt.RT.ppsubst subst));
+ let term = rt.RT.apply_subst subst term in
+ debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
+ (match rt.RT.type_of_aux' metasenv [] term ugraph with
+ | RT.Success (term, ty, metasenv, ugraph) ->
+ let body_metasenv, lambdas_metasenv =
+ split_metasenv metasenv spline_len
+ in
+ let term = purge_unused_lambdas lambdas_metasenv term in
+ debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
+ term, ugraph
+ | RT.Exception s -> debug_print s; raise UnableToCompose)
+ | RT.Exception s -> debug_print s; raise UnableToCompose
+ in