(* $Id: cicCoercion.ml 7077 2006-12-05 15:44:54Z fguidi $ *)
-let debug = false
+let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
(* given the new coercion uri from src to tgt returns the list
coercions
in
(HExtlib.flatten_map
- (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
+ (fun (_,t,ul) ->
+ if CoercDb.eq_carr ~exact:true src t then [] else
+ List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @
(HExtlib.flatten_map
- (fun (s,_,ul) -> List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
+ (fun (s,_,ul) ->
+ if CoercDb.eq_carr ~exact:true s tgt then [] else
+ List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @
(HExtlib.flatten_map
(fun (s,_,u1l) ->
HExtlib.flatten_map
(fun (_,t,u2l) ->
HExtlib.flatten_map
(fun u1 ->
+ if CoercDb.eq_carr ~exact:true s t then [] else
List.map
(fun u2 -> (s,[u1;uri;u2],t))
u2l)
(* generate_composite (c2 (c1 s)) in the universe graph univ
* 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 original_metasenv = metasenv 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
in
let compose c1 nc1 c2 nc2 =
Cic.Lambda
- (Cic.Name "x", (Cic.Implicit None),
+ (Cic.Name "x", (Cic.Implicit (Some `Type)),
(Cic.Appl ( CicSubstitution.lift 1 c2 :: mk_implicits nc2 @
[ Cic.Appl ( CicSubstitution.lift 1 c1 :: mk_implicits nc1 @
[if last_lam_with_inn_arg then Cic.Rel 1 else Cic.Implicit None])
List.sort
(fun (i,ctx1,ty1) (j,ctx1,ty1) ->
try List.assoc i meta2no - List.assoc j meta2no
- with Not_found ->
- assert false)
+ with Not_found -> assert false)
body_metasenv
in
let namer l n =
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 old_insert_coercions = !CicRefine.insert_coercions in
let c, metasenv, univ =
try
+ CicRefine.insert_coercions := false;
let term, ty, metasenv, ugraph =
CicRefine.type_of_aux' metasenv context c univ
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
+ let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
let term, ty, metasenv, ugraph =
CicRefine.type_of_aux' metasenv context term ugraph
let body_metasenv, lambdas_metasenv =
split_metasenv metasenv (spline_len + List.length context)
in
+ let lambdas_metasenv =
+ List.filter
+ (fun (i,_,_) ->
+ List.for_all (fun (j,_,_) -> i <> j) original_metasenv)
+ lambdas_metasenv
+ in
let term = purge_unused_lambdas lambdas_metasenv term in
+ let metasenv =
+ List.filter
+ (fun (i,_,_) ->
+ List.for_all
+ (fun (j,_,_) ->
+ i <> j || List.exists (fun (j,_,_) -> j=i) original_metasenv)
+ lambdas_metasenv)
+ metasenv
+ in
debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
debug_print(lazy("MENV: "^CicMetaSubst.ppmetasenv [] metasenv));
+ CicRefine.insert_coercions := old_insert_coercions;
term, metasenv, ugraph
with
| CicRefine.RefineFailure s
| CicRefine.Uncertain s -> debug_print s;
+ CicRefine.insert_coercions := old_insert_coercions;
raise UnableToCompose
+ | exn ->
+ CicRefine.insert_coercions := old_insert_coercions;
+ raise exn
in
c, metasenv, univ
;;
if List.exists (UriManager.eq uri) l then retry ()
else
try
- let _ = Http_getter.resolve' ~writable:true uri in
- if Http_getter.exists' uri then retry () else uri
+ let _ = Http_getter.resolve' ~local:true ~writable:true uri in
+ if Http_getter.exists' ~local:true uri then retry () else uri
with
| Http_getter_types.Key_not_found _ -> uri
| Http_getter_types.Unresolvable_URI _ -> assert false
(* given a new coercion uri from src to tgt returns
* a list of (new coercion uri, coercion obj, universe graph)
*)
-let close_coercion_graph _ src tgt uri baseuri =
+let close_coercion_graph src tgt uri baseuri =
(* check if the coercion already exists *)
let coercions = CoercDb.to_list () in
let todo_list = get_closure_coercions src tgt uri coercions in
(CoercDb.term_of_carr (CoercDb.Uri coer))
[] [] univ arity true
in
- assert (menv = []);
+ if (menv = []) then
+ HLog.warn "MENV non empty after composing coercions";
build_obj t univ arity
| _ -> assert false
) (first_step, CicUniv.empty_ugraph) tl