;;
(* searches a coercion fron src to tgt in the !coercions list *)
-let look_for_coercion' metasenv subst context src tgt =
+let look_for_coercion_carr metasenv subst context src tgt =
let is_dead = function CoercDb.Dead -> true | _ -> false in
let pp_l s l =
match l with
| ul -> SomeCoercion (saturate_coercion ul metasenv subst context))
;;
+let rec count_pi c s t =
+ match CicReduction.whd ~delta:false ~subst:s c t with
+ | Cic.Prod (_,_,t) -> 1 + count_pi c s t
+ | _ -> 0
+;;
+
let look_for_coercion metasenv subst context src tgt =
- let src_uri = CoercDb.coerc_carr_of_term src 0 in
- let tgt_uri = CoercDb.coerc_carr_of_term tgt 0 in
- look_for_coercion' metasenv subst context src_uri tgt_uri
+ let src_arity = count_pi context subst src in
+ let tgt_arity = count_pi context subst tgt in
+ let src_carr = CoercDb.coerc_carr_of_term src src_arity in
+ let tgt_carr = CoercDb.coerc_carr_of_term tgt tgt_arity in
+ look_for_coercion_carr metasenv subst context src_carr tgt_carr
let source_of t =
match CoercDb.is_a_coercion t with
| [] -> acc
;;
-let meets metasenv subst context left right =
+let meets metasenv subst context (grow_left,left) (grow_right,right) =
let saturate metasenv uo =
match uo with
| None -> metasenv, None
in
List.map
(fun (c,uo1,uo2) ->
- let metasenv, uo1 = saturate metasenv uo1 in
- let metasenv, uo2 = saturate metasenv uo2 in
+ let metasenv, uo1 =
+ if grow_left then saturate metasenv uo1 else metasenv, None in
+ let metasenv, uo2 =
+ if grow_right then saturate metasenv uo2 else metasenv, None in
c,metasenv, uo1, uo2)
(min [] (intersect (grow left) (grow right)))
;;