- | C.Meta (i,l)::args, _ ->
- let subst,metasenv,t2' =
- beta_expand_many test_equality_only metasenv subst context t2 args
- in
- subst,metasenv,t1,t2'
- | _, C.Meta (i,l)::args ->
- let subst,metasenv,t1' =
- beta_expand_many test_equality_only metasenv subst context t1 args
- in
- subst,metasenv,t1',t2
+----------------- *)
+ (* andrea: this case should be probably rewritten in the
+ 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
+ let exists_a_meta l =
+ List.exists (function Cic.Meta _ -> true | _ -> false) l
+ in
+ (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 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.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 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.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 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)