X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=ed650a3c326cd5dedc0ff605f877a638a024453c;hb=94c6cfe7e6b833190904c6b546668d716978a812;hp=71203b3a5dccdf2b3c5207677f2df501c6eb4084;hpb=fed8f1a2c4d10e8b6411ae471d0f85636d2f13a9;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 71203b3a5..ed650a3c3 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -143,7 +143,6 @@ let rec lambda_intros rdb metasenv subst context t args = List.map (fun arg -> arg, NCicTypeChecker.typeof ~metasenv ~subst context arg) args in let context_of_args = context in - let mk_appl = function [] -> assert false | [t] -> t | l -> NCic.Appl l in let rec mk_lambda metasenv subst context n processed_args = function | [] -> let metasenv, _, bo, _ = @@ -155,20 +154,17 @@ let rec lambda_intros rdb metasenv subst context t args = let name = "HBeta"^string_of_int n in let metasenv,_,instance,_ = NCicMetaSubst.mk_meta metasenv context_of_args `Term in - let meta_applied = mk_appl (instance::List.rev processed_args) in + let meta_applied = + NCicUntrusted.mk_appl instance (List.rev processed_args) in let metasenv,subst,_,_ = !refiner_typeof ((rdb :> NRstatus.status)#set_coerc_db NCicCoercion.empty_db) metasenv subst context_of_args meta_applied None in -prerr_endline ("########################## LI1: " ^ NCicPp.ppterm ~metasenv ~subst ~context:context_of_args meta_applied ^ " vs " ^ NCicPp.ppterm ~metasenv ~subst ~context:context_of_args ty); -prerr_endline (NCicPp.ppcontext ~metasenv ~subst context_of_args); -prerr_endline (NCicPp.ppmetasenv metasenv ~subst); let metasenv,subst = unify rdb true metasenv subst context_of_args meta_applied ty in -prerr_endline "UNIFY FINITA"; let telescopic_ty = NCicSubstitution.lift n instance in let telescopic_ty = - mk_appl (telescopic_ty :: mk_irl (List.length processed_args)) in -prerr_endline ("########################## LI: " ^ NCicPp.ppterm ~metasenv ~subst ~context telescopic_ty); + NCicUntrusted.mk_appl + telescopic_ty (mk_irl (List.length processed_args)) in let metasenv, subst, bo = mk_lambda metasenv subst ((name,NCic.Decl telescopic_ty)::context) (n+1) (arg::processed_args) tail @@ -348,13 +344,10 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = | _, NCic.Meta (n, _) when is_locked n subst -> (let (metasenv, subst), i = match NCicReduction.whd ~subst context t1 with - | NCic.Appl (NCic.Meta (i,l)::args) when - not (NCicMetaSubst.flexible subst args) - -> + | NCic.Appl (NCic.Meta (i,l)::args) -> let metasenv, subst, lambda_Mj = lambda_intros rdb metasenv subst context t1 args in -prerr_endline ("XXXXXXXXX " ^ NCicPp.ppterm ~metasenv ~subst ~context lambda_Mj); unify rdb test_eq_only metasenv subst context (C.Meta (i,l)) lambda_Mj, i @@ -429,45 +422,41 @@ prerr_endline ("XXXXXXXXX " ^ NCicPp.ppterm ~metasenv ~subst ~context lambda_Mj) with Invalid_argument _ -> raise (fail_exc metasenv subst context t1 t2)) - | NCic.Appl (NCic.Meta (i,l)::args), _ when - not (NCicMetaSubst.flexible subst args) -> - (* we verify that none of the args is a Meta, - since beta expanding w.r.t a metavariable makes no sense *) - let metasenv, subst, lambda_Mj = - lambda_intros rdb metasenv subst context t1 args - in - let metasenv, subst = - unify rdb test_eq_only metasenv subst context - (C.Meta (i,l)) lambda_Mj - in - let metasenv, subst = - unify rdb test_eq_only metasenv subst context t1 t2 - in - (try - let name, ctx, term, ty = NCicUtils.lookup_subst i subst in - let term = eta_reduce subst term in - let subst = List.filter (fun (j,_) -> j <> i) subst in - metasenv, ((i, (name, ctx, term, ty)) :: subst) - with Not_found -> assert false) - - | _, NCic.Appl (NCic.Meta (i,l)::args) when - not(NCicMetaSubst.flexible subst args) -> - let metasenv, subst, lambda_Mj = - lambda_intros rdb metasenv subst context t2 args - in - let metasenv, subst = - unify rdb test_eq_only metasenv subst context - lambda_Mj (C.Meta (i,l)) - in - let metasenv, subst = - unify rdb test_eq_only metasenv subst context t1 t2 - in - (try - let name, ctx, term, ty = NCicUtils.lookup_subst i subst in - let term = eta_reduce subst term in - let subst = List.filter (fun (j,_) -> j <> i) subst in - metasenv, ((i, (name, ctx, term, ty)) :: subst) - with Not_found -> assert false) + | NCic.Appl (NCic.Meta (i,l)::args), _ -> + let metasenv, subst, lambda_Mj = + lambda_intros rdb metasenv subst context t1 args + in + let metasenv, subst = + unify rdb test_eq_only metasenv subst context + (C.Meta (i,l)) lambda_Mj + in + let metasenv, subst = + unify rdb test_eq_only metasenv subst context t1 t2 + in + (try + let name, ctx, term, ty = NCicUtils.lookup_subst i subst in + let term = eta_reduce subst term in + let subst = List.filter (fun (j,_) -> j <> i) subst in + metasenv, ((i, (name, ctx, term, ty)) :: subst) + with Not_found -> assert false) + + | _, NCic.Appl (NCic.Meta (i,l)::args) -> + let metasenv, subst, lambda_Mj = + lambda_intros rdb metasenv subst context t2 args + in + let metasenv, subst = + unify rdb test_eq_only metasenv subst context + lambda_Mj (C.Meta (i,l)) + in + let metasenv, subst = + unify rdb test_eq_only metasenv subst context t1 t2 + in + (try + let name, ctx, term, ty = NCicUtils.lookup_subst i subst in + let term = eta_reduce subst term in + let subst = List.filter (fun (j,_) -> j <> i) subst in + metasenv, ((i, (name, ctx, term, ty)) :: subst) + with Not_found -> assert false) (* processing this case here we avoid a useless small delta step *) | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))