- let sop,subst''',metasenv''',ugraph3 =
- sort_of_prod subst'' metasenv''
- context (name,s') (sort1,sort2) ugraph2
- in
- C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
+ (try
+ let sop,subst''',metasenv''',ugraph3 =
+ sort_of_prod subst'' metasenv''
+ context (name,s') (sort1,sort2) ugraph2
+ in
+ C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
+ with
+ | RefineFailure _ as exn ->
+ (* given [t] of type [type_to_coerce] returns
+ * a term that has type [tgt_sort] eventually
+ * derived from (coercion [t]) *)
+ let refined_target = t' in
+ let sort_of_refined_target = sort2 in
+ let carr t subst context = CicMetaSubst.apply_subst subst t in
+ let coerce_to_sort tgt_sort t type_to_coerce subst ctx =
+ match type_to_coerce with
+ | Cic.Sort _ -> t
+ | term ->
+ let coercion_src = carr type_to_coerce subst ctx in
+ let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
+ let search = CoercGraph.look_for_coercion in
+ (match search coercion_src coercion_tgt with
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ -> raise exn
+ | CoercGraph.NotMetaClosed ->
+ raise (Uncertain "Coercions on metas")
+ | CoercGraph.SomeCoercion c -> Cic.Appl [c;t])
+ in
+ (* this is probably not the best... *)
+ let tgt_sort_for_pi_source = Cic.Type(CicUniv.fresh()) in
+ let tgt_sort_for_pi_target = Cic.Type(CicUniv.fresh()) in
+ let new_src =
+ coerce_to_sort tgt_sort_for_pi_source s sort1 subst context
+ in
+ let context_with_new_src =
+ ((Some (name,(C.Decl new_src)))::context)
+ in
+ let new_tgt =
+ coerce_to_sort
+ tgt_sort_for_pi_target
+ refined_target sort_of_refined_target
+ subst context_with_new_src
+ in
+ let newprod = C.Prod (name,new_src,new_tgt) in
+ let _,sort_of_refined_prod,subst,metasenv,ugraph3 =
+ type_of_aux subst metasenv context newprod ugraph2
+ in
+ (* this if for a coercion on the tail of the arrow *)
+ let new_target =
+ match sort_of_refined_target with
+ | Cic.Sort _ -> refined_target
+ | _ -> new_tgt
+ in
+ C.Prod(name,new_src,new_target),
+ sort_of_refined_prod,subst,metasenv,ugraph3)