(* ||M|| This file is part of HELM, an Hypertextual, Electronic ||A|| Library of Mathematics, developed at the Computer Science ||T|| Department, University of Bologna, Italy. ||I|| ||T|| HELM is free software; you can redistribute it and/or ||A|| modify it under the terms of the GNU General Public License \ / version 2 or (at your option) any later version. \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) (* $Id$ *) exception UnificationFailure of string Lazy.t;; exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; let (===) x y = Pervasives.compare x y = 0 ;; let uncert_exc metasenv subst context t1 t2 = Uncertain (lazy ( "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " with " ^ NCicPp.ppterm ~metasenv ~subst ~context 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) ;; 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 = try NCicSubstitution.psubst ~avoid_beta_redexes:true (fun () -> raise WrongShape) [()] body with WrongShape -> orig 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 ;; module C = NCic;; module Ref = NReference;; 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);; *) 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' = 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 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 and instantiate test_eq_only metasenv subst context n lc t swap = (*D*) inside 'I'; try let rc = 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 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 = try NCicMetaSubst.delift metasenv subst context n lc t with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg) | NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg) in (* 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 (* 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 let metasenv = List.filter (fun (m,_) -> not (n = m)) metasenv in 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 = 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); if t1 === t2 then metasenv, subst else match (t1,t2) with | (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) | (C.Sort (C.Type a), C.Sort (C.Type b)) -> if NCicEnvironment.universe_eq a b then metasenv, subst else raise (fail_exc metasenv subst context t1 t2) | (C.Sort C.Prop,C.Sort (C.Type _)) -> if (not test_eq_only) then metasenv, subst else raise (fail_exc 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 | (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 context = (name1, C.Def (s1,ty1))::context in unify 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 let l1 = NCicUtils.expand_local_context l1 in let l2 = NCicUtils.expand_local_context l2 in let metasenv, subst, to_restrict, _ = List.fold_right2 (fun t1 t2 (metasenv, subst, to_restrict, i) -> try let metasenv, subst = unify test_eq_only metasenv subst context (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2) in metasenv, subst, to_restrict, i-1 with UnificationFailure _ | Uncertain _ -> 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 with | Invalid_argument _ -> assert false | NCicMetaSubst.MetaSubstFailure msg -> try 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 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg)) | 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 with NCicUtils.Subst_not_found _-> instantiate test_eq_only metasenv subst context n lc 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 with NCicUtils.Subst_not_found _-> instantiate test_eq_only metasenv subst context n lc 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 | _, 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) | 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) (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) -> (* 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 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 in unify test_eq_only metasenv subst context beta_expanded (C.Meta (i,l)) (* 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)) when Ref.eq r1 r2 -> 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 HExtlib.mk_list false lno @ relevance | _ -> relevance in let metasenv, subst, _ = try List.fold_left2 (fun (metasenv, subst, relevance) 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 with UnificationFailure _ | Uncertain _ when not b -> metasenv, subst in metasenv, subst, relevance) (metasenv, subst, relevance) tl1 tl2 with Invalid_argument _ -> raise (uncert_exc metasenv subst context t1 t2) in metasenv, subst | (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 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 let is_prop = match remove_prods ~subst [] ty with | 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 let metasenv, subst = try unify 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) (metasenv, subst) pl1 pl2 with Invalid_argument _ -> raise (uncert_exc metasenv subst context t1 t2)) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | _ -> raise (uncert_exc metasenv subst context t1 t2) (*D*) in outside(); rc with exn -> outside (); raise exn 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 | _ -> 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 *) in let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) = let h1 = height_of t1 in let h2 = height_of t2 in let delta = if flexible [t1] then max 0 (h2 - 1) else if flexible [t2] 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 if (m1' == m1 && m2' == m2 && delta > 0) then (* if we have as heads a Fix of height n>m>0 and another term of height * m, we set delta = m. The Fix may or may not reduce, depending on its * rec argument. if no reduction was performed we decrease delta to m-1 * to reduce the other term *) let delta = delta - 1 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 else m1', m2', delta = 0 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) ^ " === " ^ NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2)); let relevance = [] (* TO BE UNDERSTOOD match t1 with | C.Const r -> NCicEnvironment.get_relevance r | _ -> [] *) in let unif_from_stack t1 t2 b metasenv subst = try let t1 = NCicReduction.from_stack t1 in let t2 = NCicReduction.from_stack t2 in unif_machines metasenv subst (put_in_whd t1 t2) with UnificationFailure _ | Uncertain _ when not b -> metasenv, subst in let rec check_stack l1 l2 r (metasenv, subst) = 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) | 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)) 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 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 ;; let unify = 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)) ;; *)