+ src, tgt
+ | t ->
+ debug (lazy (
+ NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t));
+ assert false
+ in
+ index_coercion status "foo" c src tgt arity arg
+ with
+ | NCicEnvironment.BadDependency _
+ | NCicTypeChecker.TypeCheckerFailure _ -> status)
+ status clist)
+ status (CoercDb.to_list odb)
+;;
+
+let look_for_coercion status metasenv subst context infty expty =
+ let db_src,db_tgt = status#coerc_db in
+ match
+ NCicUntrusted.apply_subst subst context infty,
+ NCicUntrusted.apply_subst subst context expty
+ with
+ | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)),
+ (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> []
+ | infty, expty ->
+
+ debug (lazy ("LOOK FOR COERCIONS: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |===> " ^
+ NCicPp.ppterm ~metasenv ~subst ~context expty));
+
+ let src_class = infty :: NCicUnifHint.eq_class_of status infty in
+ let tgt_class = expty :: NCicUnifHint.eq_class_of status expty in
+
+ let set_src =
+ List.fold_left
+ (fun set infty ->
+ CoercionSet.union (DB.retrieve_unifiables db_src infty) set)
+ CoercionSet.empty src_class
+ in
+ let set_tgt =
+ List.fold_left
+ (fun set expty ->
+ CoercionSet.union (DB.retrieve_unifiables db_tgt expty) set)
+ CoercionSet.empty tgt_class
+ in
+
+ debug (lazy ("CANDIDATES SRC: " ^
+ String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+ name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
+ (CoercionSet.elements set_src))));
+ debug (lazy ("CANDIDATES TGT: " ^
+ String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+ name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
+ (CoercionSet.elements set_tgt))));
+
+ let candidates = CoercionSet.inter set_src set_tgt in
+
+ debug (lazy ("CANDIDATES: " ^
+ String.concat "," (List.map (fun (name,t,_,_,_,_) ->
+ name ^ " :: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)
+ (CoercionSet.elements candidates))));
+
+ List.map
+ (fun (name,t,arity,arg,_,_) ->
+ let ty =
+ try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t
+ with NCicTypeChecker.TypeCheckerFailure s ->
+ prerr_endline ("illtyped coercion: "^Lazy.force s);
+ prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
+ assert false
+ in
+ let ty, metasenv, args =
+ NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
+ in
+
+ debug (lazy (
+ NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^
+ NCicPp.ppterm ~metasenv ~subst ~context
+ (NCicUntrusted.mk_appl t args) ^ " --- " ^
+ string_of_int (List.length args) ^ " == " ^ string_of_int arg));
+
+ name,metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
+ (CoercionSet.elements candidates)
+;;
+
+(* CSC: very inefficient implementation!
+ Enrico, can we use a discrimination tree here? *)
+let match_coercion status ~metasenv ~subst ~context t =
+ let db =
+ DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) []
+ in
+ (HExtlib.list_findopt
+ (fun (_,p,arity,cpos,_,_) _ ->
+ try
+ let t =
+ match p,t with
+ NCic.Appl lp, NCic.Appl lt ->
+ (match fst (HExtlib.split_nth (List.length lp) lt) with
+ [t] -> t
+ | l -> NCic.Appl l)
+ | _,NCic.Appl (he::_) -> he
+ | _,_ -> t
+ in
+ let b = NCicReduction.alpha_eq metasenv subst context p t in
+ if not b then None else
+ let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] p in
+ let pis =
+ let rec aux = function NCic.Prod (_,_,t) -> 1+aux t | _ -> 0 in
+ aux ty
+ in
+ Some (p,pis - arity - cpos - 1,cpos)
+ with
+ Failure _ -> None (* raised by split_nth *)
+ ) db)