From: Enrico Tassi Date: Fri, 31 Aug 2007 08:44:56 +0000 (+0000) Subject: fixed coercions between arrows when the arrow is dependent. X-Git-Tag: 0.4.95@7852~233 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=447c96d72448a6876e29b1d0b39400a139fa0be0;p=helm.git fixed coercions between arrows when the arrow is dependent. --- diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 2ef492bc8..9ccf2b2ff 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -1408,37 +1408,34 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il if not allow_coercions || not !insert_coercions then enrich localization_tbl t exn else - let clean t subst context = - CicReduction.whd - ~delta:false context (CicMetaSubst.apply_subst subst t) - in + let whd = CicReduction.whd ~delta:false in + let clean t s c = whd c (CicMetaSubst.apply_subst s t) in let infty = clean infty subst context in let expty = clean expty subst context in match infty, expty with | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2) -> - (* covariant part *) + let module CS = CicSubstitution in let name_con = Cic.Name "name_con" in - let name_t, ty_s_bo, bo = + let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in + (* contravariant part: the argument of f:src->ty *) + let (rel1, _), subst, metasenv, ugraph = + coerce_to_something_aux + (Cic.Rel 1) (CS.lift 1 src2) + (CS.lift 1 src) subst metasenv context_src2 ugraph + in + (* covariant part: the result of f(c x); x:src2; (c x):src *) + let name_t, bo = match t with - | Cic.Lambda (name, src, bo) -> name, src, bo - | _ -> name_con,src,Cic.Appl[CicSubstitution.lift 1 t;Cic.Rel 1] + | Cic.Lambda (n,_,bo) -> n, CS.subst rel1 (CS.lift_from 2 1 bo) + | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1] in - let context_bo = (Some (name_t, Cic.Decl ty_s_bo)) :: context in + (* we fix the possible dependency problem in the source ty *) + let ty = CS.subst rel1 (CS.lift_from 2 1 ty) in let (bo, _), subst, metasenv, ugraph = coerce_to_something_aux - bo ty ty2 subst metasenv context_bo ugraph - in - (* contravariant part *) - let context_rel1 = (Some (name_t, Cic.Decl src2) :: context) in - let (rel1, _), subst, metasenv, ugraph = - coerce_to_something_aux - (Cic.Rel 1) (CicSubstitution.lift 1 src2) - (CicSubstitution.lift 1 src) subst metasenv context_rel1 ugraph - in - let coerced = - Cic.Lambda (name_t,src2, - CicSubstitution.subst rel1 (CicSubstitution.lift_from 2 1 bo)) + bo ty ty2 subst metasenv context_src2 ugraph in + let coerced = Cic.Lambda (name_t,src2, bo) in (coerced, expty), subst, metasenv, ugraph | _ -> coerce_atom_to_something t infty expty subst metasenv context ugraph