+ let order_body_menv term body_metasenv =
+ let rec purge_lambdas = function
+ | Cic.Lambda (_,_,t) -> purge_lambdas t
+ | t -> t
+ in
+ let skip_appl = function | Cic.Appl l -> List.tl l | _ -> assert false in
+ let metas_that_saturate l =
+ List.fold_left
+ (fun (acc,n) t ->
+ let metas = CicUtil.metas_of_term t in
+ let metas = List.map fst metas in
+ let metas =
+ List.filter
+ (fun i -> List.for_all (fun (j,_) -> j<>i) acc)
+ metas
+ in
+ let metas = List.map (fun i -> i,n) metas in
+ metas @ acc, n+1)
+ ([],0) l
+ in
+ let l_c2 = skip_appl (purge_lambdas term) in
+ let l_c1 =
+ match HExtlib.list_last l_c2 with
+ | Cic.Appl l -> List.tl l
+ | _ -> assert false
+ in
+ (* i should cut off the laet elem of l_c2 *)
+ let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in
+ List.sort
+ (fun (i,ctx1,ty1) (j,ctx1,ty1) ->
+ try List.assoc i meta2no - List.assoc j meta2no
+ with Not_found -> assert false)
+ body_metasenv
+ in
+ let namer l n =
+ let l = List.map (function Cic.Name s -> s | _ -> "A") l in
+ let l = List.fold_left
+ (fun acc s ->
+ let rec add' s =
+ if List.exists ((=) s) acc then add' (s^"'") else s
+ in
+ acc@[add' s])
+ [] l
+ in
+ let l = List.rev l in
+ Cic.Name (List.nth l (n-1))
+ 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, names_c1 = count_saturations_needed c1_ty arity in
+ let saturations_for_c2, names_c2 = count_saturations_needed c2_ty 0 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 (namer (names_c1 @ names_c2)) 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 body_metasenv = order_body_menv term body_metasenv in
+ debug_print(lazy("ORDERED_B_MENV: "^rt.RT.ppmetasenv [] body_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