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=90a5d3ce63d7e81c94028136e0ed188e1a5c0bc8;hpb=e6c30351b99a9732c0aa5df361d1510b998afb76;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 90a5d3ce6..09d9ede47 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -29,42 +29,52 @@ let fail_exc metasenv subst context t1 t2 = " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2)); ;; -let mk_appl hd tl = - match hd with - | NCic.Appl l -> NCic.Appl (l@tl) - | _ -> NCic.Appl (hd :: tl) -;; - -let flexible l = - List.exists - (function - | NCic.Meta _ - | NCic.Appl (NCic.Meta _::_) -> true - | _ -> false) l +let mk_appl ~upto hd tl = + NCicReduction.head_beta_reduce ~upto + (match hd with + | NCic.Appl l -> NCic.Appl (l@tl) + | _ -> NCic.Appl (hd :: tl)) ;; 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;; @@ -72,11 +82,9 @@ let indent = ref "";; let inside c = indent := !indent ^ String.make 1 c;; let outside () = indent := String.sub !indent 0 (String.length !indent -1);; -(* let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) ;; -*) let pp _ = ();; @@ -99,74 +107,40 @@ let fix_sorts swap metasenv subst context meta t = aux () t ;; -let rec beta_expand 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 test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg) - else - unify 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 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 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 *) - -and instantiate test_eq_only metasenv subst context n lc t swap = +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 = pp (lazy(string_of_int n ^ " :=?= "^ NCicPp.ppterm ~metasenv ~subst ~context t)); let unify test_eq_only m s c t1 t2 = - if swap then unify test_eq_only m s c t2 t1 - else unify test_eq_only m s c t1 t2 + if swap then unify hdb test_eq_only m s c t2 t1 + else unify hdb test_eq_only m s c t1 t2 in let name, ctx, ty = NCicUtils.lookup_meta n metasenv in let metasenv, subst, t = @@ -205,17 +179,32 @@ and instantiate 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) @@ -245,16 +234,21 @@ and instantiate test_eq_only metasenv subst context n lc t swap = metasenv, subst (*D*) in outside(); rc with exn -> outside (); raise exn -and unify test_eq_only metasenv subst context t1 t2 = - (*D*) inside 'U'; try let rc = +and unify hdb test_eq_only metasenv subst context t1 t2 = + (*D*) inside 'U'; try let rc = let fo_unif test_eq_only metasenv subst t1 t2 = (*D*) inside 'F'; try let rc = - pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ - NCicPp.ppterm ~metasenv ~subst ~context t2)); + pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ + NCicPp.ppterm ~metasenv ~subst ~context t2 ^ "\n" ^ NCicPp.ppmetasenv + ~subst metasenv)); if t1 === t2 then metasenv, subst else match (t1,t2) with + | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl [] + | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) -> + prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant"; + assert false | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> if NCicEnvironment.universe_leq a b then metasenv, subst else raise (fail_exc metasenv subst context t1 t2) @@ -267,13 +261,13 @@ and unify test_eq_only metasenv subst context t1 t2 = | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> - let metasenv, subst = unify true metasenv subst context s1 s2 in - unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 + let metasenv, subst = unify hdb true metasenv subst context s1 s2 in + unify hdb test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) -> - let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in - let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in + let metasenv,subst=unify hdb test_eq_only metasenv subst context ty1 ty2 in + let metasenv,subst=unify hdb test_eq_only metasenv subst context s1 s2 in let context = (name1, C.Def (s1,ty1))::context in - unify test_eq_only metasenv subst context t1 t2 + unify hdb test_eq_only metasenv subst context t1 t2 | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 -> (try @@ -284,7 +278,7 @@ and unify test_eq_only metasenv subst context t1 t2 = (fun t1 t2 (metasenv, subst, to_restrict, i) -> try let metasenv, subst = - unify test_eq_only metasenv subst context + unify hdb test_eq_only metasenv subst context (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2) in metasenv, subst, to_restrict, i-1 @@ -305,64 +299,117 @@ and unify test_eq_only metasenv subst context t1 t2 = let _,_,term,_ = NCicUtils.lookup_subst n1 subst in let term1 = NCicSubstitution.subst_meta lc1 term in let term2 = NCicSubstitution.subst_meta lc2 term in - unify test_eq_only metasenv subst context term1 term2 + 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 let _,_,term,_ = NCicUtils.lookup_subst n subst in let term = NCicSubstitution.subst_meta lc term in - unify test_eq_only metasenv subst context term t + unify hdb test_eq_only metasenv subst context term t with NCicUtils.Subst_not_found _-> - instantiate test_eq_only metasenv subst context n lc t false) + instantiate hdb test_eq_only metasenv subst context n lc + (NCicReduction.head_beta_reduce ~subst t) false) | t, C.Meta (n,lc) -> (try let _,_,term,_ = NCicUtils.lookup_subst n subst in let term = NCicSubstitution.subst_meta lc term in - unify test_eq_only metasenv subst context t term + unify hdb test_eq_only metasenv subst context t term with NCicUtils.Subst_not_found _-> - instantiate test_eq_only metasenv subst context n lc t true) + instantiate hdb test_eq_only metasenv subst context n lc + (NCicReduction.head_beta_reduce ~subst t) true) | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst -> let _,_,term,_ = NCicUtils.lookup_subst i subst in let term = NCicSubstitution.subst_meta l term in - unify test_eq_only metasenv subst context (mk_appl term args) t2 + unify hdb test_eq_only metasenv subst context + (mk_appl ~upto:(List.length args) term args) t2 | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst -> let _,_,term,_ = NCicUtils.lookup_subst i subst in let term = NCicSubstitution.subst_meta l term in - unify test_eq_only metasenv subst context t1 (mk_appl term args) + unify hdb test_eq_only metasenv subst context t1 + (mk_appl ~upto:(List.length args) term args) | NCic.Appl (NCic.Meta (i,_)::_ as l1), NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j -> (try List.fold_left2 (fun (metasenv, subst) t1 t2 -> - unify test_eq_only metasenv subst context t1 t2) + unify hdb test_eq_only metasenv subst context t1 t2) (metasenv,subst) l1 l2 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 - test_eq_only false - metasenv subst context t2 args + let metasenv, lambda_Mj = + lambda_intros metasenv subst context t1 args in - unify 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 - test_eq_only true - metasenv subst context t1 args + let metasenv, subst = + unify hdb test_eq_only metasenv subst context + (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 - unify test_eq_only metasenv subst context - beta_expanded (C.Meta (i,l)) + let metasenv, subst = + unify hdb test_eq_only metasenv subst context + 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)) @@ -370,7 +417,10 @@ and unify 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 @@ -381,7 +431,7 @@ and unify test_eq_only metasenv subst context t1 t2 = let b, relevance = match relevance with b::tl -> b,tl | _ -> true, [] in let metasenv, subst = - try unify test_eq_only metasenv subst context t1 t2 + try unify hdb test_eq_only metasenv subst context t1 t2 with UnificationFailure _ | Uncertain _ when not b -> metasenv, subst in @@ -394,13 +444,13 @@ and unify test_eq_only metasenv subst context t1 t2 = | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1), C.Match (ref2,outtype2,term2,pl2)) -> - let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in - let _,_,ty,_ = List.nth itl tyno in - let rec remove_prods ~subst context ty = + let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in + let _,_,ty,_ = List.nth itl tyno in + let rec remove_prods ~subst context ty = let ty = NCicReduction.whd ~subst context ty in match ty with | C.Sort _ -> ty - | C.Prod (name,so,ta) -> + | C.Prod (name,so,ta) -> remove_prods ~subst ((name,(C.Decl so))::context) ta | _ -> assert false in @@ -409,28 +459,20 @@ and unify test_eq_only metasenv subst context t1 t2 = | C.Sort C.Prop -> true | _ -> false in - let rec remove_prods ~subst context ty = - let ty = NCicReduction.whd ~subst context ty in - match ty with - | C.Sort _ -> ty - | C.Prod (name,so,ta) -> - remove_prods ~subst ((name,(C.Decl so))::context) ta - | _ -> assert false - in if not (Ref.eq ref1 ref2) then raise (uncert_exc metasenv subst context t1 t2) else let metasenv, subst = - unify test_eq_only metasenv subst context outtype1 outtype2 in + unify hdb test_eq_only metasenv subst context outtype1 outtype2 in let metasenv, subst = - try unify test_eq_only metasenv subst context term1 term2 + try unify hdb test_eq_only metasenv subst context term1 term2 with UnificationFailure _ | Uncertain _ when is_prop -> metasenv, subst in (try List.fold_left2 (fun (metasenv,subst) -> - unify test_eq_only metasenv subst context) + unify hdb test_eq_only metasenv subst context) (metasenv, subst) pl1 pl2 with Invalid_argument _ -> raise (uncert_exc metasenv subst context t1 t2)) @@ -441,6 +483,47 @@ and unify test_eq_only metasenv subst context t1 t2 = | _ -> raise (uncert_exc metasenv subst context t1 t2) (*D*) in outside(); rc with exn -> outside (); raise exn in + let try_hints metasenv subst t1 t2 (* exc*) = +(* + 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),premises)::tl -> +(* + 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 = + 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 _ -> + cand_iter tl + in + cand_iter candidates + in let height_of = function | NCic.Const (Ref.Ref (_,Ref.Def h)) | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h))) @@ -452,7 +535,7 @@ and unify test_eq_only metasenv subst context t1 t2 = NCicReduction.reduce_machine ~delta:max_int ~subst context m1, NCicReduction.reduce_machine ~delta:max_int ~subst context m2 in - let small_delta_step + let small_delta_step ~subst ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2) = assert (not (norm1 && norm2)); @@ -471,12 +554,13 @@ and unify test_eq_only metasenv subst context t1 t2 = function | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) -> (*D*) inside 'M'; try let rc = -(* - pp (lazy((if are_normal then "*" else " ") ^ " " ^ - NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^ + pp (lazy("UM: " ^ + NCicPp.ppterm ~metasenv ~subst ~context + (NCicReduction.unwind (k1,e1,t1,s1)) ^ " === " ^ - NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2))); -*) + NCicPp.ppterm ~metasenv ~subst ~context + (NCicReduction.unwind (k2,e2,t2,s2)))); +pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2)); let relevance = [] (* TO BE UNDERSTOOD match t1 with | C.Const r -> NCicEnvironment.get_relevance r @@ -489,37 +573,48 @@ and unify test_eq_only metasenv subst context t1 t2 = with UnificationFailure _ | Uncertain _ when not b -> metasenv, subst in - let rec check_stack l1 l2 r (metasenv, subst) = + let rec check_stack l1 l2 r todo = match l1,l2,r with - | x1::tl1, x2::tl2, r::tr -> - check_stack tl1 tl2 tr - (unif_from_stack x1 x2 r metasenv subst) - | x1::tl1, x2::tl2, [] -> - check_stack tl1 tl2 [] - (unif_from_stack x1 x2 true metasenv subst) + | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo) + | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo) | l1, l2, _ -> - fo_unif test_eq_only metasenv subst - (NCicReduction.unwind (k1,e1,t1,List.rev l1)) - (NCicReduction.unwind (k2,e2,t2,List.rev l2)) + NCicReduction.unwind (k1,e1,t1,List.rev l1), + NCicReduction.unwind (k2,e2,t2,List.rev l2), + todo in - try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst) + let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in + try + let metasenv,subst = fo_unif test_eq_only metasenv subst hh1 hh2 in + List.fold_left + (fun (metasenv,subst) (x1,x2,r) -> + unif_from_stack x1 x2 r metasenv subst + ) (metasenv,subst) todo with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) -> - unif_machines metasenv subst (small_delta_step m1 m2) + unif_machines metasenv subst (small_delta_step ~subst m1 m2) (*D*) in outside(); rc with exn -> outside (); raise exn in try fo_unif test_eq_only metasenv subst t1 t2 - with UnificationFailure msg | Uncertain msg as exn -> - try - unif_machines metasenv subst - (put_in_whd (0,[],t1,[]) (0,[],t2,[])) - with - | UnificationFailure _ -> raise (UnificationFailure msg) - | Uncertain _ -> raise exn + with + | UnificationFailure msg as exn -> + (try + unif_machines metasenv subst + (put_in_whd (0,[],t1,[]) (0,[],t2,[])) + with + | UnificationFailure _ -> raise (UnificationFailure msg) + | Uncertain _ -> raise exn) + | Uncertain msg as exn -> + match try_hints metasenv subst t1 t2 with + | Some x -> x + | None -> + try + unif_machines metasenv subst + (put_in_whd (0,[],t1,[]) (0,[],t2,[])) + with + | UnificationFailure _ -> raise (UnificationFailure msg) + | Uncertain _ -> raise exn (*D*) in outside(); rc with exn -> outside (); raise exn ;; -let unify = +let unify hdb ?(test_eq_only=false) = indent := ""; - unify false;; - - + unify hdb test_eq_only;;