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;;
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)
| (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
(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
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 ->
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))
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
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
| (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
| 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))
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 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 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
+ 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
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<BEGIN>%s\n<END>" (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<BEGIN>%s\n<END>" (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<BEGIN>%s\n<END>" (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<BEGIN>%s\n<END>" (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;;
projects / helm.git / blobdiff