- spirit of deref *)
- let rec beta_reduce =
- function
- (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
- let he'' = CicSubstitution.subst he' t in
- if tl' = [] then
- he''
- else
- beta_reduce (Cic.Appl(he''::tl'))
- | t -> t in
- (match l1,l2 with
- C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
- (try
- List.fold_left2
- (fun (subst,metasenv) ->
- fo_unif_subst test_equality_only subst context metasenv)
- (subst,metasenv) l1 l2
- with (Invalid_argument msg) -> raise (UnificationFailure msg))
- | C.Meta (i,l)::args, _ ->
- (try
- let (_,t) = CicUtil.lookup_subst i subst in
- let lifted = S.lift_meta l t in
- let reduced = beta_reduce (Cic.Appl (lifted::args)) in
- fo_unif_subst
- test_equality_only
- subst context metasenv reduced t2
- with CicUtil.Subst_not_found _ ->
- let subst,metasenv,beta_expanded =
- beta_expand_many
- test_equality_only metasenv subst context t2 args in
- fo_unif_subst test_equality_only subst context metasenv
- (C.Meta (i,l)) beta_expanded)
- | _, C.Meta (i,l)::args ->
- (try
- let (_,t) = CicUtil.lookup_subst i subst in
- let lifted = S.lift_meta l t in
- let reduced = beta_reduce (Cic.Appl (lifted::args)) in
- fo_unif_subst
- test_equality_only
- subst context metasenv t1 reduced
- with CicUtil.Subst_not_found _ ->
- let subst,metasenv,beta_expanded =
- beta_expand_many
- test_equality_only metasenv subst context t1 args in
- fo_unif_subst test_equality_only subst context metasenv
- (C.Meta (i,l)) beta_expanded)
- | _,_ ->
- let lr1 = List.rev l1 in
- let lr2 = List.rev l2 in
- let rec fo_unif_l test_equality_only subst metasenv =
- function
- [],_
- | _,[] -> assert false
- | ([h1],[h2]) ->
- fo_unif_subst test_equality_only subst context metasenv h1 h2
- | ([h],l)
- | (l,[h]) ->
- fo_unif_subst test_equality_only subst context metasenv
- h (C.Appl (List.rev l))
- | ((h1::l1),(h2::l2)) ->
- let subst', metasenv' =
- fo_unif_subst test_equality_only subst context metasenv h1 h2
- in
- fo_unif_l test_equality_only subst' metasenv' (l1,l2)
- in
- fo_unif_l test_equality_only subst metasenv (lr1, lr2) )
+ spirit of deref *)
+ (match l1,l2 with
+ | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
+ (try
+ List.fold_left2
+ (fun (subst,metasenv,ugraph) t1 t2 ->
+ fo_unif_subst
+ test_equality_only subst context metasenv t1 t2 ugraph)
+ (subst,metasenv,ugraph) l1 l2
+ with (Invalid_argument msg) ->
+ raise (UnificationFailure (lazy msg)))
+ | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
+ (* we verify that none of the args is a Meta,
+ since beta expanding with respoect to a metavariable
+ makes no sense *)
+ (*
+ (try
+ let (_,t,_) = CicUtil.lookup_subst i subst in
+ let lifted = S.subst_meta l t in
+ let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
+ fo_unif_subst
+ test_equality_only
+ subst context metasenv reduced t2 ugraph
+ with CicUtil.Subst_not_found _ -> *)
+ let subst,metasenv,beta_expanded,ugraph1 =
+ beta_expand_many
+ test_equality_only metasenv subst context t2 args ugraph
+ in
+ fo_unif_subst test_equality_only subst context metasenv
+ (C.Meta (i,l)) beta_expanded ugraph1
+ | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
+ (* (try
+ let (_,t,_) = CicUtil.lookup_subst i subst in
+ let lifted = S.subst_meta l t in
+ let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
+ fo_unif_subst
+ test_equality_only
+ subst context metasenv t1 reduced ugraph
+ with CicUtil.Subst_not_found _ -> *)
+ let subst,metasenv,beta_expanded,ugraph1 =
+ beta_expand_many
+ test_equality_only
+ metasenv subst context t1 args ugraph
+ in
+ fo_unif_subst test_equality_only subst context metasenv
+ (C.Meta (i,l)) beta_expanded ugraph1
+ | _,_ ->
+ let lr1 = List.rev l1 in
+ let lr2 = List.rev l2 in
+ let rec
+ fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
+ match (l1,l2) with
+ [],_
+ | _,[] -> assert false
+ | ([h1],[h2]) ->
+ fo_unif_subst
+ test_equality_only subst context metasenv h1 h2 ugraph
+ | ([h],l)
+ | (l,[h]) ->
+ fo_unif_subst test_equality_only subst context metasenv
+ h (C.Appl (List.rev l)) ugraph
+ | ((h1::l1),(h2::l2)) ->
+ let subst', metasenv',ugraph1 =
+ fo_unif_subst
+ test_equality_only
+ subst context metasenv h1 h2 ugraph
+ in
+ fo_unif_l
+ test_equality_only subst' metasenv' (l1,l2) ugraph1
+ in
+ (try
+ fo_unif_l
+ test_equality_only subst metasenv (lr1, lr2) ugraph
+ with
+ | UnificationFailure _
+ | Uncertain _ as exn ->
+ (match l1, l2 with
+ | (((Cic.Const (uri1, ens1)) as c1) :: tl1),
+ (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
+ CoercGraph.is_a_coercion c1 &&
+ CoercGraph.is_a_coercion c2 ->
+ let body1, attrs1, ugraph =
+ match CicEnvironment.get_obj ugraph uri1 with
+ | Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
+ | _ -> assert false
+ in
+ let body2, attrs2, ugraph =
+ match CicEnvironment.get_obj ugraph uri2 with
+ | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
+ | _ -> assert false
+ in
+ let is_composite1 =
+ List.exists ((=) (`Class `Coercion)) attrs1 in
+ let is_composite2 =
+ List.exists ((=) (`Class `Coercion)) attrs2 in
+ (match is_composite1, is_composite2 with
+ | false, false -> raise exn
+ | true, false ->
+ let body1 = CicSubstitution.subst_vars ens1 body1 in
+ let appl = Cic.Appl (body1::tl1) in
+ let redappl = CicReduction.head_beta_reduce appl in
+ fo_unif_subst
+ test_equality_only subst context metasenv
+ redappl t2 ugraph
+ | false, true ->
+ let body2 = CicSubstitution.subst_vars ens2 body2 in
+ let appl = Cic.Appl (body2::tl2) in
+ let redappl = CicReduction.head_beta_reduce appl in
+ fo_unif_subst
+ test_equality_only subst context metasenv
+ t1 redappl ugraph
+ | true, true ->
+ let body1 = CicSubstitution.subst_vars ens1 body1 in
+ let appl1 = Cic.Appl (body1::tl1) in
+ let redappl1 = CicReduction.head_beta_reduce appl1 in
+ let body2 = CicSubstitution.subst_vars ens2 body2 in
+ let appl2 = Cic.Appl (body2::tl2) in
+ let redappl2 = CicReduction.head_beta_reduce appl2 in
+ fo_unif_subst
+ test_equality_only subst context metasenv
+ redappl1 redappl2 ugraph)
+ | _ -> raise exn)))