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=99286591d9c2f01c0b67f5f362bccf6f4ebec482;hpb=1ef41da37d7b39da1521f53d3b22981556bfbe68;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 99286591d..09d9ede47 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -26,45 +26,55 @@ let uncert_exc metasenv subst context t1 t2 = let fail_exc metasenv subst context t1 t2 = UnificationFailure (lazy ( "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ - " 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) + " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2)); ;; -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,122 +82,173 @@ 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 ^ " " ^ s);; -*) + prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) +;; let pp _ = ();; -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 fix_sorts swap metasenv subst context meta t = + let rec aux () = function + | NCic.Sort (NCic.Type u) as orig -> + if swap then + match NCicEnvironment.sup u with + | None -> prerr_endline "no sup for" ; + raise (fail_exc metasenv subst context meta t) + | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1) + else + NCic.Sort (NCic.Type ( + match NCicEnvironment.sup NCicEnvironment.type0 with + | Some x -> x + | _ -> assert false)) + | NCic.Meta _ as orig -> orig + | t -> NCicUtils.map (fun _ _ -> ()) () aux t + in + aux () 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 (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 ("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 test_eq_only metasenv subst context n lc t swap = -(*D*) inside 'I'; try let rc = +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 - in - let ty_t = - try NCicTypeChecker.typeof ~subst ~metasenv context t - with NCicTypeChecker.TypeCheckerFailure msg -> - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t); - prerr_endline (Lazy.force msg); - assert false + 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 lty = NCicSubstitution.subst_meta lc ty in - pp ("On the types: " ^ 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 + let metasenv, subst, t = + match ty with + | NCic.Implicit (`Typeof _) -> + metasenv,subst, t + (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *) + | _ -> + pp (lazy ( + "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^ + NCicPp.ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^ + NCicPp.ppmetasenv ~subst metasenv)); + let t, ty_t = + try t, NCicTypeChecker.typeof ~subst ~metasenv context t + with + | NCicTypeChecker.AssertFailure msg -> + (pp (lazy "fine typeof (fallimento)"); + let ft=fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t in + if ft == t then + (prerr_endline ( ("ILLTYPED: " ^ + NCicPp.ppterm ~metasenv ~subst ~context t + ^ "\nBECAUSE:" ^ Lazy.force msg ^ "\nCONTEXT:\n" ^ + NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^ + NCicPp.ppmetasenv ~subst metasenv + )); + assert false) + else + try + pp (lazy ("typeof: " ^ + NCicPp.ppterm ~metasenv ~subst ~context ft)); + ft, NCicTypeChecker.typeof ~subst ~metasenv context ft + with NCicTypeChecker.AssertFailure _ -> + assert false) + | NCicTypeChecker.TypeCheckerFailure msg -> + prerr_endline (Lazy.force msg); + pp msg; assert false + in + let lty = NCicSubstitution.subst_meta lc ty in + 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 - with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg) - | NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg) + 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) + | NCicMetaSubst.MetaSubstFailure msg -> + pp (lazy ("delift fails: " ^ Lazy.force msg)); + raise (UnificationFailure msg) in + pp (lazy(string_of_int n ^ " := 222 = "^ + NCicPp.ppterm ~metasenv ~subst ~context:ctx t + ^ "\n" ^ NCicPp.ppmetasenv ~subst metasenv)); (* Unifying the types may have already instantiated n. *) try let _, _,oldt,_ = NCicUtils.lookup_subst n subst in let oldt = NCicSubstitution.subst_meta lc oldt in + let t = NCicSubstitution.subst_meta lc t in (* conjecture: always fail --> occur check *) unify test_eq_only metasenv subst context oldt t with NCicUtils.Subst_not_found _ -> (* by cumulativity when unify(?,Type_i) * we could ? := Type_j with j <= i... *) let subst = (n, (name, ctx, t, ty)) :: subst in + pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm + ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t))); let metasenv = List.filter (fun (m,_) -> not (n = m)) metasenv in metasenv, subst -(*D*) in outside(); rc with exn -> outside (); raise exn + (*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 (" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ - NCicPp.ppterm ~metasenv ~subst ~context t2); + (*D*) inside 'F'; try let rc = + 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) @@ -200,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 @@ -217,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 @@ -225,10 +286,12 @@ and unify test_eq_only metasenv subst context t1 t2 = metasenv, subst, i::to_restrict, i-1) l1 l2 (metasenv, subst, [], List.length l1) in - let metasenv, subst, _ = - NCicMetaSubst.restrict metasenv subst n1 to_restrict - in - metasenv, subst + if to_restrict <> [] then + let metasenv, subst, _ = + NCicMetaSubst.restrict metasenv subst n1 to_restrict + in + metasenv, subst + else metasenv, subst with | Invalid_argument _ -> assert false | NCicMetaSubst.MetaSubstFailure msg -> @@ -236,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 + let metasenv, subst = + unify hdb test_eq_only metasenv subst context + lambda_Mj (C.Meta (i,l)) 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 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)) @@ -301,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 @@ -312,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 @@ -325,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 @@ -340,73 +459,108 @@ 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)) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false + | _ when NCicUntrusted.metas_of_term subst context t1 = [] && + NCicUntrusted.metas_of_term subst context t2 = [] -> + raise (fail_exc metasenv subst context t1 t2) | _ -> raise (uncert_exc metasenv subst context t1 t2) - (*D*) in outside(); rc with exn -> outside (); raise exn + (*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))) | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_) - | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h, false - | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> 0, true - | _ -> 0, false + | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h + | _ -> 0 in let put_in_whd m1 m2 = NCicReduction.reduce_machine ~delta:max_int ~subst context m1, - NCicReduction.reduce_machine ~delta:max_int ~subst context m2, - false (* not in normal form *) + NCicReduction.reduce_machine ~delta:max_int ~subst context m2 in - let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) = - let h1, flex1 = height_of t1 in - let h2, flex2 = height_of t2 in - let delta = - if flex1 then max 0 (h2 - 1) else - if flex2 then max 0 (h1 - 1) else - if h1 = h2 then max 0 (h1 -1) else min h1 h2 - in - pp ("DELTA STEP TO: " ^ string_of_int delta); - let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in - let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in - m1', m2', (m1' == m1 && m2' == m2) || delta = 0 - (* if we have as heads two Fix of height n>0, they may or may not - * reduce, depending on their rec argument... we thus check if - * something changed or not. This relies on the reduction machine - * preserving the original machine if it performs no action *) + let small_delta_step ~subst + ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2) + = + assert (not (norm1 && norm2)); + if norm1 then + x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2 + else if norm2 then + NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2 + else + let h1 = height_of t1 in + let h2 = height_of t2 in + let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in + NCicReduction.reduce_machine ~delta ~subst context m1, + NCicReduction.reduce_machine ~delta ~subst context m2 in let rec unif_machines metasenv subst = function - | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),are_normal) -> - (*D*) inside 'M'; try let rc = - pp ((if are_normal then "*" else " ") ^ " " ^ - NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^ + | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) -> + (*D*) inside 'M'; try let rc = + 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 @@ -419,981 +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) - with UnificationFailure _ | Uncertain _ when not are_normal -> -(* - let delta = delta - 1 in - let red = NCicReduction.reduce_machine ~delta ~subst context in -*) - unif_machines metasenv subst (small_delta_step m1 m2) - (*D*) in outside(); rc with exn -> outside (); raise exn + 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 ~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 -(*D*) in outside(); rc with exn -> outside (); 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;; - - - -(* - -open Printf - -exception UnificationFailure of string Lazy.t;; -exception Uncertain of string Lazy.t;; -exception AssertFailure of string Lazy.t;; - -let verbose = false;; -let debug_print = fun _ -> () - -let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'" -let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand" -let profiler_deref = HExtlib.profile "fo_unif_subst.deref'" -let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible" - -let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'" - -let type_of_aux' metasenv subst context term ugraph = -let foo () = - try - profile.HExtlib.profile - (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph - with - CicTypeChecker.TypeCheckerFailure msg -> - let msg = - lazy - (sprintf - "Kernel Type checking error: -%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad." - (CicMetaSubst.ppterm ~metasenv subst term) - (CicMetaSubst.ppterm ~metasenv [] term) - (CicMetaSubst.ppcontext ~metasenv subst context) - (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in - raise (AssertFailure msg) - | CicTypeChecker.AssertFailure msg -> - let msg = lazy - (sprintf - "Kernel Type checking assertion failure: -%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad." - (CicMetaSubst.ppterm ~metasenv subst term) - (CicMetaSubst.ppterm ~metasenv [] term) - (CicMetaSubst.ppcontext ~metasenv subst context) - (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in - raise (AssertFailure msg) -in profiler_toa.HExtlib.profile foo () -;; - -let exists_a_meta l = - List.exists - (function - | Cic.Meta _ - | Cic.Appl (Cic.Meta _::_) -> true - | _ -> false) l - -let rec deref subst t = - let snd (_,a,_) = a in - match t with - Cic.Meta(n,l) -> - (try - deref subst - (CicSubstitution.subst_meta - l (snd (CicUtil.lookup_subst n subst))) - with - CicUtil.Subst_not_found _ -> t) - | Cic.Appl(Cic.Meta(n,l)::args) -> - (match deref subst (Cic.Meta(n,l)) with - | Cic.Lambda _ as t -> - deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args))) - | r -> Cic.Appl(r::args)) - | Cic.Appl(((Cic.Lambda _) as t)::args) -> - deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args))) - | t -> t -;; - -let deref subst t = - let foo () = deref subst t - in profiler_deref.HExtlib.profile foo () - -exception WrongShape;; -let eta_reduce after_beta_expansion after_beta_expansion_body - before_beta_expansion - = - try - match before_beta_expansion,after_beta_expansion_body with - Cic.Appl l, Cic.Appl l' -> - let rec all_but_last check_last = - function - [] -> assert false - | [Cic.Rel 1] -> [] - | [_] -> if check_last then raise WrongShape else [] - | he::tl -> he::(all_but_last check_last tl) - in - let all_but_last check_last l = - match all_but_last check_last l with - [] -> assert false - | [he] -> he - | l -> Cic.Appl l - in - let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in - let all_but_last = all_but_last false l in - (* here we should test alpha-equivalence; however we know by - construction that here alpha_equivalence is equivalent to = *) - if t = all_but_last then - all_but_last - else - after_beta_expansion - | _,_ -> after_beta_expansion - with - WrongShape -> after_beta_expansion - -let rec beta_expand num test_equality_only metasenv subst context t arg ugraph = - let module S = CicSubstitution in - let module C = Cic in -let foo () = - let rec aux metasenv subst n context t' ugraph = - try - - let subst,metasenv,ugraph1 = - fo_unif_subst test_equality_only subst context metasenv - (CicSubstitution.lift n arg) t' ugraph - - in - subst,metasenv,C.Rel (1 + n),ugraph1 - with - Uncertain _ - | UnificationFailure _ -> - match t' with - | C.Rel m -> subst,metasenv, - (if m <= n then C.Rel m else C.Rel (m+1)),ugraph - | C.Var (uri,exp_named_subst) -> - let subst,metasenv,exp_named_subst',ugraph1 = - aux_exp_named_subst metasenv subst n context exp_named_subst ugraph - in - subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1 - | C.Meta (i,l) -> - (* 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 *) - let l = - List.map - (function - Some t -> Some (CicSubstitution.lift 1 t) - | None -> None) l in - subst, metasenv, C.Meta (i,l), ugraph - | C.Sort _ - | C.Implicit _ as t -> subst,metasenv,t,ugraph - | C.Cast (te,ty) -> - let subst,metasenv,te',ugraph1 = - aux metasenv subst n context te ugraph in - let subst,metasenv,ty',ugraph2 = - aux metasenv subst n context ty ugraph1 in - (* TASSI: sure this is in serial? *) - subst,metasenv,(C.Cast (te', ty')),ugraph2 - | C.Prod (nn,s,t) -> - let subst,metasenv,s',ugraph1 = - aux metasenv subst n context s ugraph in - let subst,metasenv,t',ugraph2 = - aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t - ugraph1 - in - (* TASSI: sure this is in serial? *) - subst,metasenv,(C.Prod (nn, s', t')),ugraph2 - | C.Lambda (nn,s,t) -> - let subst,metasenv,s',ugraph1 = - aux metasenv subst n context s ugraph in - let subst,metasenv,t',ugraph2 = - aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1 - in - (* TASSI: sure this is in serial? *) - subst,metasenv,(C.Lambda (nn, s', t')),ugraph2 - | C.LetIn (nn,s,ty,t) -> - let subst,metasenv,s',ugraph1 = - aux metasenv subst n context s ugraph in - let subst,metasenv,ty',ugraph1 = - aux metasenv subst n context ty ugraph in - let subst,metasenv,t',ugraph2 = - aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t - ugraph1 - in - (* TASSI: sure this is in serial? *) - subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2 - | C.Appl l -> - let subst,metasenv,revl',ugraph1 = - List.fold_left - (fun (subst,metasenv,appl,ugraph) t -> - let subst,metasenv,t',ugraph1 = - aux metasenv subst n context t ugraph in - subst,metasenv,(t'::appl),ugraph1 - ) (subst,metasenv,[],ugraph) l - in - subst,metasenv,(C.Appl (List.rev revl')),ugraph1 - | C.Const (uri,exp_named_subst) -> - let subst,metasenv,exp_named_subst',ugraph1 = - aux_exp_named_subst metasenv subst n context exp_named_subst ugraph - in - subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1 - | C.MutInd (uri,i,exp_named_subst) -> - let subst,metasenv,exp_named_subst',ugraph1 = - aux_exp_named_subst metasenv subst n context exp_named_subst ugraph - in - subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1 - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let subst,metasenv,exp_named_subst',ugraph1 = - aux_exp_named_subst metasenv subst n context exp_named_subst ugraph - in - subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1 - | C.MutCase (sp,i,outt,t,pl) -> - let subst,metasenv,outt',ugraph1 = - aux metasenv subst n context outt ugraph in - let subst,metasenv,t',ugraph2 = - aux metasenv subst n context t ugraph1 in - let subst,metasenv,revpl',ugraph3 = - List.fold_left - (fun (subst,metasenv,pl,ugraph) t -> - let subst,metasenv,t',ugraph1 = - aux metasenv subst n context t ugraph in - subst,metasenv,(t'::pl),ugraph1 - ) (subst,metasenv,[],ugraph2) pl - in - subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3 - (* TASSI: not sure this is serial *) - | C.Fix (i,fl) -> -(*CSC: not implemented - let tylen = List.length fl in - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo)) - fl - in - C.Fix (i, substitutedfl) -*) - subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph - | C.CoFix (i,fl) -> -(*CSC: not implemented - let tylen = List.length fl in - let substitutedfl = - List.map - (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo)) - fl - in - C.CoFix (i, substitutedfl) - -*) - subst,metasenv,(CicSubstitution.lift 1 t'), ugraph - - and aux_exp_named_subst metasenv subst n context ens ugraph = - List.fold_right - (fun (uri,t) (subst,metasenv,l,ugraph) -> - let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in - subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph) - in - let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in - let fresh_name = - FreshNamesGenerator.mk_fresh_name ~subst - metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty - in - let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in - let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in - subst, metasenv, t'', ugraph2 -in profiler_beta_expand.HExtlib.profile foo () - - -and beta_expand_many test_equality_only metasenv subst context t args ugraph = - let _,subst,metasenv,hd,ugraph = - List.fold_right - (fun arg (num,subst,metasenv,t,ugraph) -> - let subst,metasenv,t,ugraph1 = - beta_expand num test_equality_only - metasenv subst context t arg ugraph - in - num+1,subst,metasenv,t,ugraph1 - ) args (1,subst,metasenv,t,ugraph) - in - subst,metasenv,hd,ugraph - -and warn_if_not_unique xxx to1 to2 carr car1 car2 = - match xxx with - | [] -> () - | (m2,_,c2,c2')::_ -> - let m1,c1,c1' = carr,to1,to2 in - let unopt = - function Some (_,t) -> CicPp.ppterm t - | None -> "id" - in - HLog.warn - ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^ - CoercDb.string_of_carr car2^": " ^ - CoercDb.string_of_carr m1^" via "^unopt c1^" + "^ - unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^ - unopt c2^" + "^unopt c2') - -(* NUOVA UNIFICAZIONE *) -(* A substitution is a (int * Cic.term) list that associates a - metavariable i with its body. - A metaenv is a (int * Cic.term) list that associate a metavariable - i with is type. - fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back - a new substitution which is _NOT_ unwinded. It must be unwinded before - applying it. *) - -and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph = - let module C = Cic in - let module R = CicReduction in - let module S = CicSubstitution in - let t1 = deref subst t1 in - let t2 = deref subst t2 in - let (&&&) a b = (a && b) || ((not a) && (not b)) in -(* let bef = Sys.time () in *) - let b,ugraph = - if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then - false,ugraph - else -let foo () = - R.are_convertible ~subst ~metasenv context t1 t2 ugraph -in profiler_are_convertible.HExtlib.profile foo () - in -(* let aft = Sys.time () in -if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^ -CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^ -CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *) - if b then - subst, metasenv, ugraph - else - match (t1, t2) with - | (C.Meta (n,ln), C.Meta (m,lm)) when n=m -> - let _,subst,metasenv,ugraph1 = - (try - List.fold_left2 - (fun (j,subst,metasenv,ugraph) t1 t2 -> - match t1,t2 with - None,_ - | _,None -> j+1,subst,metasenv,ugraph - | Some t1', Some t2' -> - (* First possibility: restriction *) - (* Second possibility: unification *) - (* Third possibility: convertibility *) - let b, ugraph1 = - R.are_convertible - ~subst ~metasenv context t1' t2' ugraph - in - if b then - j+1,subst,metasenv, ugraph1 - else - (try - let subst,metasenv,ugraph2 = - fo_unif_subst - test_equality_only - subst context metasenv t1' t2' ugraph - in - j+1,subst,metasenv,ugraph2 - with - Uncertain _ - | UnificationFailure _ -> -debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j))); - let metasenv, subst = - CicMetaSubst.restrict - subst [(n,j)] metasenv in - j+1,subst,metasenv,ugraph1) - ) (1,subst,metasenv,ugraph) ln lm - with - Exit -> - raise - (UnificationFailure (lazy "1")) - (* - (sprintf - "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted." - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2))) *) - | Invalid_argument _ -> - raise - (UnificationFailure (lazy "2"))) - (* - (sprintf - "Error trying to unify %s with %s: the lengths of the two local contexts do not match." - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) *) - in subst,metasenv,ugraph1 - | (C.Meta (n,_), C.Meta (m,_)) when n>m -> - fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph - | (C.Meta (n,l), t) - | (t, C.Meta (n,l)) -> - let swap = - match t1,t2 with - C.Meta (n,_), C.Meta (m,_) when n < m -> false - | _, C.Meta _ -> false - | _,_ -> true - in - let lower = fun x y -> if swap then y else x in - let upper = fun x y -> if swap then x else y in - let fo_unif_subst_ordered - test_equality_only subst context metasenv m1 m2 ugraph = - fo_unif_subst test_equality_only subst context metasenv - (lower m1 m2) (upper m1 m2) ugraph - in - begin - let subst,metasenv,ugraph1 = - let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in - (try - let tyt,ugraph1 = - type_of_aux' metasenv subst context t ugraph - in - fo_unif_subst - test_equality_only - subst context metasenv tyt (S.subst_meta l meta_type) ugraph1 - with - UnificationFailure _ as e -> raise e - | Uncertain msg -> raise (UnificationFailure msg) - | AssertFailure _ -> - debug_print (lazy "siamo allo huge hack"); - (* TODO huge hack!!!! - * we keep on unifying/refining in the hope that - * the problem will be eventually solved. - * In the meantime we're breaking a big invariant: - * the terms that we are unifying are no longer well - * typed in the current context (in the worst case - * we could even diverge) *) - (subst, metasenv,ugraph)) in - let t',metasenv,subst = - try - CicMetaSubst.delift n subst context metasenv l t - with - (CicMetaSubst.MetaSubstFailure msg)-> - raise (UnificationFailure msg) - | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) - in - let t'',ugraph2 = - match t' with - C.Sort (C.Type u) when not test_equality_only -> - let u' = CicUniv.fresh () in - let s = C.Sort (C.Type u') in - (try - let ugraph2 = - CicUniv.add_ge (upper u u') (lower u u') ugraph1 - in - s,ugraph2 - with - CicUniv.UniverseInconsistency msg -> - raise (UnificationFailure msg)) - | _ -> t',ugraph1 - in - (* Unifying the types may have already instantiated n. Let's check *) - try - let (_, oldt,_) = CicUtil.lookup_subst n subst 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 - CicUtil.Subst_not_found _ -> - let (_, context, ty) = CicUtil.lookup_meta n metasenv in - let subst = (n, (context, t'',ty)) :: subst in - let metasenv = - List.filter (fun (m,_,_) -> not (n = m)) metasenv in - subst, metasenv, ugraph2 - end - | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2)) - | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) -> - if UriManager.eq uri1 uri2 then - fo_unif_subst_exp_named_subst test_equality_only subst context metasenv - exp_named_subst1 exp_named_subst2 ugraph - else - raise (UnificationFailure (lazy - (sprintf - "Can't unify %s with %s due to different constants" - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) - | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) -> - if UriManager.eq uri1 uri2 && i1 = i2 then - fo_unif_subst_exp_named_subst - test_equality_only - subst context metasenv exp_named_subst1 exp_named_subst2 ugraph - else - raise (UnificationFailure - (lazy - (sprintf - "Can't unify %s with %s due to different inductive principles" - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) - | C.MutConstruct (uri1,i1,j1,exp_named_subst1), - C.MutConstruct (uri2,i2,j2,exp_named_subst2) -> - if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then - fo_unif_subst_exp_named_subst - test_equality_only - subst context metasenv exp_named_subst1 exp_named_subst2 ugraph - else - raise (UnificationFailure - (lazy - (sprintf - "Can't unify %s with %s due to different inductive constructors" - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) - | (C.Implicit _, _) | (_, C.Implicit _) -> assert false - | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only - subst context metasenv te t2 ugraph - | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only - subst context metasenv t1 te ugraph - | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> - let subst',metasenv',ugraph1 = - fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph - in - fo_unif_subst test_equality_only - subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 - | (C.LetIn (_,s1,ty1,t1), t2) - | (t2, C.LetIn (_,s1,ty1,t1)) -> - fo_unif_subst - test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph - | (C.Appl l1, C.Appl l2) -> - (* andrea: this case should be probably rewritten in the - spirit of deref *) - (match l1,l2 with - | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j -> - (try - List.fold_left2 - (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 (lazy msg))) - | 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.subst_meta l t in - let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in - fo_unif_subst - test_equality_only - subst context metasenv reduced t2 ugraph - with CicUtil.Subst_not_found _ -> *) - let subst,metasenv,beta_expanded,ugraph1 = - beta_expand_many - 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.subst_meta l t in - let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in - fo_unif_subst - test_equality_only - subst context metasenv t1 reduced ugraph - with CicUtil.Subst_not_found _ -> *) - let subst,metasenv,beta_expanded,ugraph1 = - beta_expand_many - 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 ugraph1 - | _,_ -> - let lr1 = List.rev l1 in - let lr2 = List.rev l2 in - let rec - fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph = - match (l1,l2) with - [],_ - | _,[] -> assert false - | ([h1],[h2]) -> - fo_unif_subst - test_equality_only subst context metasenv h1 h2 ugraph - | ([h],l) - | (l,[h]) -> - fo_unif_subst test_equality_only subst context metasenv - h (C.Appl (List.rev l)) ugraph - | ((h1::l1),(h2::l2)) -> - let subst', metasenv',ugraph1 = - fo_unif_subst - test_equality_only - subst context metasenv h1 h2 ugraph - in - fo_unif_l - test_equality_only subst' metasenv' (l1,l2) ugraph1 - in - (try - fo_unif_l - test_equality_only subst metasenv (lr1, lr2) ugraph - with - | UnificationFailure s - | Uncertain s as exn -> - (match l1, l2 with - (* {{{ pullback *) - | (((Cic.Const (uri1, ens1)) as cc1) :: tl1), - (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when - CoercDb.is_a_coercion cc1 <> None && - CoercDb.is_a_coercion cc2 <> None && - not (UriManager.eq uri1 uri2) -> -(*DEBUGGING ONLY: -prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context); -*) - let inner_coerced t = - let t = CicMetaSubst.apply_subst subst t in - let rec aux c x t = - match t with - | Cic.Appl l -> - (match CoercGraph.coerced_arg l with - | None -> c, x - | Some (t,_) -> aux (List.hd l) t t) - | _ -> c, x - in - aux (Cic.Implicit None) (Cic.Implicit None) t - in - let c1,last_tl1 = inner_coerced (Cic.Appl l1) in - let c2,last_tl2 = inner_coerced (Cic.Appl l2) in - let car1, car2 = - match - CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2 - with - | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2 - | _ -> assert false - in - let head1_c, head2_c = - match - CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2 - with - | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2 - | _ -> assert false - in - let unfold uri ens args = - let o, _ = - CicEnvironment.get_obj CicUniv.oblivion_ugraph uri - in - assert (ens = []); - match o with - | Cic.Constant (_,Some bo,_,_,_) -> - CicReduction.head_beta_reduce ~delta:false - (Cic.Appl (bo::args)) - | _ -> assert false - in - let conclude subst metasenv ugraph last_tl1' last_tl2' = - let subst',metasenv,ugraph = -(*DEBUGGING ONLY: -prerr_endline - ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ - " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context); -*) - fo_unif_subst test_equality_only subst context - metasenv last_tl1' last_tl2' ugraph - in - if subst = subst' then raise exn - else -(*DEBUGGING ONLY: -let subst,metasenv,ugrph as res = -*) - fo_unif_subst test_equality_only subst' context - metasenv (C.Appl l1) (C.Appl l2) ugraph -(*DEBUGGING ONLY: -in -(prerr_endline - (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ - " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context); -res) -*) - in - if CoercDb.eq_carr car1 car2 then - match last_tl1,last_tl2 with - | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn - | _, C.Meta _ - | C.Meta _, _ -> - let subst,metasenv,ugraph = - fo_unif_subst test_equality_only subst context - metasenv last_tl1 last_tl2 ugraph - in - fo_unif_subst test_equality_only subst context - metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph - | _ when CoercDb.eq_carr head1_c head2_c -> - (* composite VS composition + metas avoiding - * coercions not only in coerced position *) - if c1 <> cc1 && c2 <> cc2 then - conclude subst metasenv ugraph - last_tl1 last_tl2 - else - let l1, l2 = - if c1 = cc1 then - unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2) - else - Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2 - in - fo_unif_subst test_equality_only subst context - metasenv l1 l2 ugraph - | _ -> raise exn - else - let grow1 = - match last_tl1 with Cic.Meta _ -> true | _ -> false in - let grow2 = - match last_tl2 with Cic.Meta _ -> true | _ -> false in - if not (grow1 || grow2) then - (* no flexible terminals -> no pullback, but - * we still unify them, in some cases it helps *) - conclude subst metasenv ugraph last_tl1 last_tl2 - else - let meets = - CoercGraph.meets - metasenv subst context (grow1,car1) (grow2,car2) - in - (match meets with - | [] -> raise exn - | (carr,metasenv,to1,to2)::xxx -> - warn_if_not_unique xxx to1 to2 carr car1 car2; - let last_tl1',(subst,metasenv,ugraph) = - match grow1,to1 with - | true,Some (last,coerced) -> - last, - fo_unif_subst test_equality_only subst context - metasenv coerced last_tl1 ugraph - | _ -> last_tl1,(subst,metasenv,ugraph) - in - let last_tl2',(subst,metasenv,ugraph) = - match grow2,to2 with - | true,Some (last,coerced) -> - last, - fo_unif_subst test_equality_only subst context - metasenv coerced last_tl2 ugraph - | _ -> last_tl2,(subst,metasenv,ugraph) - in - conclude subst metasenv ugraph last_tl1' last_tl2') - (* }}} pullback *) - (* {{{ CSC: This is necessary because of the "elim H" tactic - where the type of H is only reducible to an - inductive type. This could be extended from inductive - types to any rigid term. However, the code is - duplicated in two places: inside applications and - outside them. Probably it would be better to - work with lambda-bar terms instead. *) - | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn - | (_, Cic.MutInd _::_) -> - let t1' = R.whd ~subst context t1 in - (match t1' with - C.Appl (C.MutInd _::_) -> - fo_unif_subst test_equality_only - subst context metasenv t1' t2 ugraph - | _ -> raise (UnificationFailure (lazy "88"))) - | (Cic.MutInd _::_,_) -> - let t2' = R.whd ~subst context t2 in - (match t2' with - C.Appl (C.MutInd _::_) -> - fo_unif_subst test_equality_only - subst context metasenv t1 t2' ugraph - | _ -> raise - (UnificationFailure - (lazy ("not a mutind :"^ - CicMetaSubst.ppterm ~metasenv subst t2 )))) - (* }}} elim H *) - | _ -> raise exn))) - | (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 - ugraph in - let subst'',metasenv'',ugraph2 = - fo_unif_subst test_equality_only subst' context metasenv' t1' t2' - ugraph1 in - (try - List.fold_left2 - (fun (subst,metasenv,ugraph) t1 t2 -> - fo_unif_subst - test_equality_only subst context metasenv t1 t2 ugraph - ) (subst'',metasenv'',ugraph2) pl1 pl2 - with - Invalid_argument _ -> - raise (UnificationFailure (lazy "6.1"))) - (* (sprintf - "Error trying to unify %s with %s: the number of branches is not the same." - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) *) - | (C.Rel _, _) | (_, C.Rel _) -> - if t1 = t2 then - subst, metasenv,ugraph - else - raise (UnificationFailure (lazy - (sprintf - "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) - | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) -> - let subst,metasenv,beta_expanded,ugraph1 = - beta_expand_many - 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 - | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) -> - let subst,metasenv,beta_expanded,ugraph1 = - beta_expand_many - test_equality_only metasenv subst context t1 args ugraph - in - fo_unif_subst test_equality_only subst context metasenv - beta_expanded (C.Meta (i,l)) ugraph1 -(* Works iff there are no arguments applied to it; similar to the - case below - | (_, C.MutInd _) -> - let t1' = R.whd ~subst context t1 in - (match t1' with - C.MutInd _ -> - fo_unif_subst test_equality_only - subst context metasenv t1' t2 ugraph - | _ -> raise (UnificationFailure (lazy "8"))) -*) - | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> - let subst',metasenv',ugraph1 = - fo_unif_subst true subst context metasenv s1 s2 ugraph - in - fo_unif_subst test_equality_only - subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 - | (C.Prod _, _) -> - (match CicReduction.whd ~subst context t2 with - | C.Prod _ as t2 -> - fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph - | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product")))) - | (_, C.Prod _) -> - (match CicReduction.whd ~subst context t1 with - | C.Prod _ as t1 -> - fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph - | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product")))) - | (_,_) -> - (* delta-beta reduction should almost never be a problem for - unification since: - 1. long computations require iota reduction - 2. it is extremely rare that a close term t1 (that could be unified - to t2) beta-delta reduces to t1' while t2 does not beta-delta - reduces in the same way. This happens only if one meta of t2 - occurs in head position during beta reduction. In this unluky - case too much reduction will be performed on t1 and unification - will surely fail. *) - let t1' = CicReduction.head_beta_reduce ~delta:true t1 in - let t2' = CicReduction.head_beta_reduce ~delta:true t2 in - if t1 = t1' && t2 = t2' then - raise (UnificationFailure - (lazy - (sprintf - "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) - else - try - fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph - with - UnificationFailure _ - | Uncertain _ -> - raise (UnificationFailure - (lazy - (sprintf - "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm ~metasenv subst t1) - (CicMetaSubst.ppterm ~metasenv subst t2)))) - -and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv - exp_named_subst1 exp_named_subst2 ugraph -= - try - List.fold_left2 - (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) -> - assert (uri1=uri2) ; - fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph - ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2 - with - Invalid_argument _ -> - let print_ens ens = - String.concat " ; " - (List.map - (fun (uri,t) -> - UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t) - ) ens) - in - raise (UnificationFailure (lazy (sprintf - "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2)))) - -(* A substitution is a (int * Cic.term) list that associates a *) -(* metavariable i with its body. *) -(* metasenv is of type Cic.metasenv *) -(* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *) -(* a new substitution which is already unwinded and ready to be applied and *) -(* a new metasenv in which some hypothesis in the contexts of the *) -(* metavariables may have been restricted. *) -let fo_unif metasenv context t1 t2 ugraph = - fo_unif_subst false [] context metasenv t1 t2 ugraph ;; - -let enrich_msg msg subst context metasenv t1 t2 ugraph = - lazy ( - if verbose then - sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s" - (CicMetaSubst.ppterm ~metasenv subst t1) - (try - let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in - CicPp.ppterm ty_t1 - with - | UnificationFailure s - | Uncertain s - | AssertFailure s -> sprintf "MALFORMED(t1): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppterm ~metasenv subst t2) - (try - let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in - CicPp.ppterm ty_t2 - with - | UnificationFailure s - | Uncertain s - | AssertFailure s -> sprintf "MALFORMED(t2): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppcontext ~metasenv subst context) - (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg) - else - sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s" - (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context) - (try - let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in - CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context - with - | UnificationFailure s - | Uncertain s - | AssertFailure s -> sprintf "MALFORMED(t1): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context) - (try - let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in - CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context - with - | UnificationFailure s - | Uncertain s - | AssertFailure s -> sprintf "MALFORMED(t2): \n%s\n" (Lazy.force s)) - (CicMetaSubst.ppcontext ~metasenv subst context) - (CicMetaSubst.ppmetasenv subst metasenv) - (Lazy.force msg) - ) - -let fo_unif_subst subst context metasenv t1 t2 ugraph = - try - fo_unif_subst false subst context metasenv t1 t2 ugraph - with - | AssertFailure msg -> - raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph)) - | UnificationFailure msg -> - raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph)) -;; -*) + unify hdb test_eq_only;;