- let subst,metasenv,t1',t2' =
- match l1,l2 with
- (* In the first two cases when we reach the next begin ... end
- section useless work is done since, by construction, the list
- of arguments will be equal.
- *)
- C.Meta (i,l)::args, _ ->
- let subst,metasenv,t2' =
- eta_expand_many test_equality_only metasenv subst context t2 args
- in
- subst,metasenv,t1,t2'
- | _, C.Meta (i,l)::args ->
- let subst,metasenv,t1' =
- eta_expand_many test_equality_only metasenv subst context t1 args
- in
- subst,metasenv,t1',t2
- | _,_ -> subst,metasenv,t1,t2
- in
- begin
- match t1',t2' with
- C.Appl l1, C.Appl l2 ->
- 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)
- | _ -> assert false
- end
+ (* andrea: this case should be probably rewritten in the
+ 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
+ fo_unif_l
+ test_equality_only subst metasenv (lr1, lr2) ugraph)