X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=09d9ede475cd12bc1a88e34fbf5be307527f1024;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=79fe81053e7e0d630efdc9ea947d2c64d0fa4df2;hpb=4573f1fecaf83f4706f39702555d5319d132477b;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 79fe81053..09d9ede47 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 "NU 1" (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,66 +107,32 @@ let fix_sorts swap metasenv subst context meta t = aux () t ;; -let rec beta_expand hdb num test_eq_only swap metasenv subst context t arg = - let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' = +let is_locked n subst = try - let metasenv, subst = - if swap then - unify hdb test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg) - else - unify hdb test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t' - in - (metasenv, subst), NCic.Rel (1 + n) - with Uncertain _ | UnificationFailure _ -> - match t' with - | NCic.Rel m as orig -> - (metasenv, subst), if m <= n then orig else NCic.Rel (m+1) - (* andrea: in general, beta_expand can create badly typed - terms. This happens quite seldom in practice, UNLESS we - iterate on the local context. For this reason, we renounce - to iterate and just lift *) - | NCic.Meta (i,(shift,lc)) -> - (metasenv,subst), NCic.Meta (i,(shift+1,lc)) - | NCic.Prod (name, src, tgt) as orig -> - let (metasenv, subst), src1 = aux (n,context,true) acc src in - let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in - let ms, tgt1 = aux k (metasenv, subst) tgt in - if src == src1 && tgt == tgt1 then ms, orig else - ms, NCic.Prod (name, src1, tgt1) - | t -> - NCicUntrusted.map_term_fold_a - (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t + match NCicUtils.lookup_subst n subst with + | Some tag, _,_,_ when NCicMetaSubst.is_out_scope_tag tag -> true + | _ -> false + with NCicUtils.Subst_not_found _ -> false +;; - in - let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in - let fresh_name = "Hbeta" ^ string_of_int num in - let (metasenv,subst), t1 = - aux (0, context, test_eq_only) (metasenv, subst) t in - let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in - try - ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2); - metasenv, subst, t2 - with NCicTypeChecker.TypeCheckerFailure _ -> - metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg) -and beta_expand_many hdb test_equality_only swap metasenv subst context t args = -(* (*D*) inside 'B'; try let rc = *) - pp (lazy (String.concat ", " - (List.map (NCicPp.ppterm ~metasenv ~subst ~context) - args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t)); - let _, subst, metasenv, hd = - List.fold_right - (fun arg (num,subst,metasenv,t) -> - let metasenv, subst, t = - beta_expand hdb num test_equality_only swap metasenv subst context t arg - in - num+1,subst,metasenv,t) - args (1,subst,metasenv,t) - in - pp (lazy ("Head syntesized by b-exp: " ^ - NCicPp.ppterm ~metasenv ~subst ~context hd)); - metasenv, subst, hd -(* (*D*) in outside (); rc with exn -> outside (); raise exn *) +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 (NCicSubstitution.lift n tty)) + in + metasenv, bo + | ty::tail -> + let name = "HBeta"^string_of_int n in + let ty = NCicSubstitution.lift n ty in + let metasenv, bo = mk_lambda ((name,NCic.Decl ty)::context) (n+1) tail in + metasenv, NCic.Lambda (name, ty, bo) + in + mk_lambda context 0 argsty and instantiate hdb test_eq_only metasenv subst context n lc t swap = (*D*) inside 'I'; try let rc = @@ -204,17 +179,32 @@ 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)); let (metasenv, subst), t = - try NCicMetaSubst.delift metasenv subst context n lc t + try + NCicMetaSubst.delift + ~unify:(fun m s c t1 t2 -> + let ind = !indent in + let res = + try Some (unify test_eq_only m s c t1 t2 ) + with UnificationFailure _ | Uncertain _ -> None + in + indent := ind; res) + metasenv subst context n lc t with NCicMetaSubst.Uncertain msg -> pp (lazy ("delift fails: " ^ Lazy.force msg)); raise (Uncertain msg) @@ -311,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 @@ -352,25 +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, subst, beta_expanded = - beta_expand_many hdb - test_eq_only false - 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 - - | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) -> - let metasenv, subst, beta_expanded = - beta_expand_many hdb - test_eq_only true - metasenv subst context t1 args + (C.Meta (i,l)) lambda_Mj + 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) + + | _, 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)) @@ -378,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 "NU 2" lno relevance) + with Failure _ -> [] + in HExtlib.mk_list false lno @ relevance | _ -> relevance in @@ -443,30 +485,41 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = in let try_hints metasenv subst t1 t2 (* exc*) = (* - prerr_endline ("\n\n\n looking for hints for : " ^ - NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ - NCicPp.ppterm ~metasenv ~subst ~context t2); + prerr_endline ("\nProblema:\n" ^ + NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^ + NCicPp.ppterm ~metasenv ~subst ~context t2); *) let candidates = NCicUnifHint.look_for_hint hdb metasenv subst context t1 t2 in let rec cand_iter = function | [] -> None (* raise exc *) - | (metasenv,c1,c2)::tl -> + | (metasenv,(c1,c2),premises)::tl -> (* - prerr_endline ("\n attempt: " ^ - NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ - NCicPp.ppterm ~metasenv ~subst ~context c1 ^ " AND " ^ - NCicPp.ppterm ~metasenv ~subst ~context c2 ^ " ==?== " ^ - NCicPp.ppterm ~metasenv ~subst ~context t2); + prerr_endline ("\nProvo il candidato:\n" ^ + String.concat "\n" + (List.map + (fun (a,b) -> + NCicPp.ppterm ~metasenv ~subst ~context a ^ " =?= " ^ + NCicPp.ppterm ~metasenv ~subst ~context b) premises) ^ + "\n-------------------------------------------\n"^ + NCicPp.ppterm ~metasenv ~subst ~context c1 ^ " = " ^ + NCicPp.ppterm ~metasenv ~subst ~context c2); *) try - let metasenv,subst = unify hdb test_eq_only metasenv subst context t1 c1 in - let metasenv,subst = unify hdb test_eq_only metasenv subst context c2 t2 in + let metasenv,subst = + fo_unif test_eq_only metasenv subst t1 c1 in + let metasenv,subst = + fo_unif test_eq_only metasenv subst c2 t2 in + let metasenv,subst = + List.fold_left + (fun (metasenv, subst) (x,y) -> + unify hdb test_eq_only metasenv subst context x y) + (metasenv, subst) premises + in Some (metasenv, subst) with UnificationFailure _ | Uncertain _ -> - prerr_endline (" outside (); raise exn ;; -let unify hdb = +let unify hdb ?(test_eq_only=false) = indent := ""; - unify hdb false;; - - + unify hdb test_eq_only;;