From eea144a45e0b58530daeb9a33f79a81a78bd3c9a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 14 Feb 2005 12:06:45 +0000 Subject: [PATCH] Added heuristic in the Appl case, we beta-expand only if the argument list does't contain metas. --- helm/ocaml/cic_unification/cicUnification.ml | 57 ++++++++------------ 1 file changed, 23 insertions(+), 34 deletions(-) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 4cfc79660..e521c6570 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -616,61 +616,50 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; 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 -(* andrea : this was too powerful. It works very bad with f_equal and - similar terms, try and see 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 + (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, _ -> -<<<<<<< cicUnification.ml - let subst,metasenv,t2',ugraph1 = - beta_expand_many test_equality_only metasenv subst context t2 args - ugraph - in - subst,metasenv,t1,t2',ugraph1 -======= + | 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 + subst context metasenv reduced t2 ugraph with CicUtil.Subst_not_found _ -> - let subst,metasenv,beta_expanded = + let subst,metasenv,beta_expanded,ugraph1 = 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) ->>>>>>> 1.40 - | _, C.Meta (i,l)::args -> -<<<<<<< cicUnification.ml - let subst,metasenv,t1',ugraph1 = - beta_expand_many test_equality_only metasenv subst context t1 args - ugraph - in - subst,metasenv,t1',t2,ugraph1 -======= + 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 + subst context metasenv t1 reduced ugraph with CicUtil.Subst_not_found _ -> - let subst,metasenv,beta_expanded = + let subst,metasenv,beta_expanded,ugraph1 = beta_expand_many - test_equality_only metasenv subst context t1 args in + 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) -*) - + (C.Meta (i,l)) beta_expanded ugraph1) | _,_ -> (* WAS BEFORE ----- <<<<<<< cicUnification.ml @@ -705,7 +694,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; test_equality_only subst' metasenv' (l1,l2) ugraph1 in fo_unif_l - test_equality_only subst metasenv (lr1, lr2) ) ugraph(*1*) + test_equality_only subst metasenv (lr1, lr2) ugraph)(**) | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> let subst', metasenv',ugraph1 = fo_unif_subst test_equality_only subst context metasenv outt1 outt2 -- 2.39.2