X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=59bc5d7e72ef9f11ee048545d11c616d367e2820;hb=9e7df95a820cb91d075f1a20d703175da874596c;hp=f23116b636d765a6460978e175da0377f0c34615;hpb=d7f32114f3806b51c2ee483dcb5a86e08d086a72;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index f23116b63..59bc5d7e7 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -36,36 +36,45 @@ let mk_appl ~upto hd tl = | _ -> NCic.Appl (hd :: tl)) ;; -let flexible l = - List.exists - (function - | NCic.Meta _ - | NCic.Appl (NCic.Meta _::_) -> true - | _ -> false) l -;; - exception WrongShape;; -let eta_reduce = - let delift_if_not_occur body orig = +let eta_reduce subst t = + let delift_if_not_occur body = try - NCicSubstitution.psubst ~avoid_beta_redexes:true - (fun () -> raise WrongShape) [()] body - with WrongShape -> orig + Some (NCicSubstitution.psubst ~avoid_beta_redexes:true + (fun () -> raise WrongShape) [()] body) + with WrongShape -> None + in + let rec eat_lambdas ctx = function + | NCic.Lambda (name, src, tgt) -> + eat_lambdas ((name, src) :: ctx) tgt + | NCic.Meta (i,lc) as t-> + (try + let _,_,t,_ = NCicUtils.lookup_subst i subst in + let t = NCicSubstitution.subst_meta lc t in + eat_lambdas ctx t + with Not_found -> ctx, t) + | t -> ctx, t in - function - | NCic.Lambda(_, _, NCic.Appl [hd; NCic.Rel 1]) as orig -> - delift_if_not_occur hd orig - | NCic.Lambda(_, _, NCic.Appl (hd :: l)) as orig - when HExtlib.list_last l = NCic.Rel 1 -> - let body = - let args, _ = HExtlib.split_nth (List.length l - 1) l in - NCic.Appl (hd::args) - in - delift_if_not_occur body orig - | t -> t + let context_body = eat_lambdas [] t in + let rec aux = function + | [],body -> body + | (name, src)::ctx, (NCic.Appl (hd::[NCic.Rel 1]) as bo) -> + (match delift_if_not_occur hd with + | None -> aux (ctx,NCic.Lambda(name,src, bo)) + | Some bo -> aux (ctx,bo)) + | (name, src)::ctx, (NCic.Appl args as bo) + when HExtlib.list_last args = NCic.Rel 1 -> + let args, _ = HExtlib.split_nth (List.length args - 1) args in + (match delift_if_not_occur (NCic.Appl args) with + | None -> aux (ctx,NCic.Lambda(name,src, bo)) + | Some bo -> aux (ctx,bo)) + | (name, src) :: ctx, t -> + aux (ctx,NCic.Lambda(name,src, t)) + in + aux context_body ;; - + module C = NCic;; module Ref = NReference;; @@ -98,13 +107,24 @@ let fix_sorts swap metasenv subst context meta t = aux () t ;; -let rec beta_expand_many metasenv subst context t args = +let is_locked n subst = + try + match NCicUtils.lookup_subst n subst with + | Some tag, _,_,_ when NCicMetaSubst.is_out_scope_tag tag -> true + | _ -> false + with NCicUtils.Subst_not_found _ -> false +;; + + +let rec lambda_intros metasenv subst context t args = let tty = NCicTypeChecker.typeof ~metasenv ~subst context t in let argsty = List.map (NCicTypeChecker.typeof ~metasenv ~subst context) args in let rec mk_lambda context n = function | [] -> let metasenv, _, bo, _ = - NCicMetaSubst.mk_meta metasenv context (`WithType tty) in + NCicMetaSubst.mk_meta metasenv context + (`WithType (NCicSubstitution.lift n tty)) + in metasenv, bo | ty::tail -> let name = "HBeta"^string_of_int n in @@ -159,12 +179,18 @@ and instantiate hdb test_eq_only metasenv subst context n lc t swap = pp msg; assert false in let lty = NCicSubstitution.subst_meta lc ty in - pp (lazy ("On the types: " ^ - NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^ - NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " - ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); - let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in - metasenv, subst, t + match ty_t with + | NCic.Implicit _ -> + raise (UnificationFailure + (lazy "trying to unify a term with a type")) + | ty_t -> + pp (lazy ("On the types: " ^ + NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^ + NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " + ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); + let metasenv,subst = + unify test_eq_only metasenv subst context lty ty_t in + metasenv, subst, t in pp (lazy(string_of_int n ^ " := 111 = "^ NCicPp.ppterm ~metasenv ~subst ~context t)); @@ -275,6 +301,35 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = let term2 = NCicSubstitution.subst_meta lc2 term in unify hdb test_eq_only metasenv subst context term1 term2 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg)) + + | _, 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) + -> + let metasenv, lambda_Mj = + lambda_intros metasenv subst context t1 args + in + unify hdb test_eq_only metasenv subst context + (C.Meta (i,l)) lambda_Mj, + i + | NCic.Meta (i,_) -> (metasenv, subst), i + | _ -> assert false + in + let t1 = NCicReduction.whd ~subst context t1 in + let j, lj = + match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false + in + let metasenv, subst = + instantiate hdb test_eq_only metasenv subst context j lj t2 true + 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)) | C.Meta (n,lc), t -> (try @@ -316,29 +371,45 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = with Invalid_argument _ -> raise (fail_exc metasenv subst context t1 t2)) - | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) -> + | 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, beta_expanded = - beta_expand_many metasenv subst context t2 args + let metasenv, lambda_Mj = + lambda_intros metasenv subst context t1 args in let metasenv, subst = unify hdb test_eq_only metasenv subst context - (C.Meta (i,l)) beta_expanded + (C.Meta (i,l)) lambda_Mj in - - (* .... eta_reduce ?i ... *) + let metasenv, subst = unify hdb 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(flexible args) -> - let metasenv, beta_expanded = - beta_expand_many metasenv subst context t1 args + | _, NCic.Appl (NCic.Meta (i,l)::args) when + not(NCicMetaSubst.flexible subst args) -> + let metasenv, lambda_Mj = + lambda_intros metasenv subst context t2 args in let metasenv, subst = unify hdb test_eq_only metasenv subst context - beta_expanded (C.Meta (i,l)) + lambda_Mj (C.Meta (i,l)) in + let metasenv, subst = unify hdb 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)) @@ -346,7 +417,10 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = let relevance = NCicEnvironment.get_relevance r1 in let relevance = match r1 with | Ref.Ref (_,Ref.Con (_,_,lno)) -> - let _,relevance = HExtlib.split_nth lno relevance in + let relevance = + try snd (HExtlib.split_nth lno relevance) + with Failure _ -> [] + in HExtlib.mk_list false lno @ relevance | _ -> relevance in @@ -541,8 +615,6 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2)); (*D*) in outside(); rc with exn -> outside (); raise exn ;; -let unify hdb = +let unify hdb ?(test_eq_only=false) = indent := ""; - unify hdb false;; - - + unify hdb test_eq_only;;