X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=130799ea432a7ee1426d7645099c0c40e6a4c5d4;hb=0575a1cb077087970f311b48f2e45dc4a01a6867;hp=4cfc796606650dfc22216c0dea6f8baf2fd51059;hpb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 4cfc79660..130799ea4 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -65,7 +65,7 @@ let rec deref subst = Cic.Meta(n,l) as t -> (try deref subst - (CicSubstitution.lift_meta + (CicSubstitution.subst_meta l (snd (CicUtil.lookup_subst n subst))) with CicUtil.Subst_not_found _ -> t) @@ -99,7 +99,7 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph = | C.Meta (i,l) as t-> (try let (_, t') = CicMetaSubst.lookup_subst i subst in - aux metasenv subst n context (CicSubstitution.lift_meta l t') + aux metasenv subst n context (CicSubstitution.subst_meta l t') ugraph with CicMetaSubst.SubstNotFound _ -> let (subst, metasenv, context, local_context,ugraph1) = @@ -417,7 +417,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str begin try let (_, oldt) = CicMetaSubst.lookup_subst n subst in - let lifted_oldt = S.lift_meta l oldt in + let lifted_oldt = S.subst_meta l oldt in let ty_lifted_oldt,ugraph1 = type_of_aux' metasenv subst context lifted_oldt ugraph in @@ -436,7 +436,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str let tyt,ugraph1 = type_of_aux' metasenv subst context t ugraph in fo_unif_subst test_equality_only - subst context metasenv tyt (S.lift_meta l meta_type) ugraph1 + subst context metasenv tyt (S.subst_meta l meta_type) ugraph1 with AssertFailure _ -> (* TODO huge hack!!!! * we keep on unifying/refining in the hope that the problem will be @@ -471,7 +471,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; (* Unifying the types may have already instantiated n. Let's check *) try let (_, oldt) = CicMetaSubst.lookup_subst n subst in - let lifted_oldt = S.lift_meta l oldt in + let lifted_oldt = S.subst_meta l oldt in fo_unif_subst_ordered test_equality_only subst context metasenv t lifted_oldt ugraph2 with @@ -495,7 +495,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; in fo_unif_subst test_equality_only - subst context metasenv tyt (S.lift_meta l meta_type) ugraph1 + subst context metasenv tyt (S.subst_meta l meta_type) ugraph1 with UnificationFailure msg | Uncertain msg -> @@ -532,7 +532,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; (* Unifying the types may have already instantiated n. Let's check *) try let (_, oldt,_) = CicUtil.lookup_subst n subst in - let lifted_oldt = S.lift_meta l oldt in + let lifted_oldt = S.subst_meta l oldt in fo_unif_subst_ordered test_equality_only subst context metasenv t lifted_oldt ugraph2 with @@ -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 lifted = S.subst_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 lifted = S.subst_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