(sprintf
"Kernel Type checking error:
%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
- (CicMetaSubst.ppterm subst term)
- (CicMetaSubst.ppterm [] term)
- (CicMetaSubst.ppcontext subst context)
+ (CicMetaSubst.ppterm ~metasenv subst term)
+ (CicMetaSubst.ppterm ~metasenv [] term)
+ (CicMetaSubst.ppcontext ~metasenv subst context)
(CicMetaSubst.ppmetasenv subst metasenv)
- (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
+ (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 subst term)
- (CicMetaSubst.ppterm [] term)
- (CicMetaSubst.ppcontext subst context)
+ (CicMetaSubst.ppterm ~metasenv subst term)
+ (CicMetaSubst.ppterm ~metasenv [] term)
+ (CicMetaSubst.ppcontext ~metasenv subst context)
(CicMetaSubst.ppmetasenv subst metasenv)
- (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
+ (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
raise (AssertFailure msg)
in profiler_toa.HExtlib.profile foo ()
;;
with
WrongShape -> after_beta_expansion
-let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
+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 () =
in
(* TASSI: sure this is in serial? *)
subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
- | C.LetIn (nn,s,t) ->
+ | 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,None)))::context) t
+ 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', t')),ugraph2
+ subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
| C.Appl l ->
let subst,metasenv,revl',ugraph1 =
List.fold_left
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") ~typ:argty
+ 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
and beta_expand_many test_equality_only metasenv subst context t args ugraph =
- let subst,metasenv,hd,ugraph =
+ let _,subst,metasenv,hd,ugraph =
List.fold_right
- (fun arg (subst,metasenv,t,ugraph) ->
+ (fun arg (num,subst,metasenv,t,ugraph) ->
let subst,metasenv,t,ugraph1 =
- beta_expand test_equality_only
+ beta_expand num test_equality_only
metasenv subst context t arg ugraph
in
- subst,metasenv,t,ugraph1
- ) args (subst,metasenv,t,ugraph)
+ num+1,subst,metasenv,t,ugraph1
+ ) args (1,subst,metasenv,t,ugraph)
in
subst,metasenv,hd,ugraph
+and warn_if_not_unique xxx car1 car2 =
+ let unopt =
+ function
+ | Some (_,Cic.Appl(Cic.Const(u,_)::_)) -> UriManager.string_of_uri u
+ | Some (_,t) -> CicPp.ppterm t
+ | None -> "id"
+ in
+ match xxx with
+ | [] -> ()
+ | _ ->
+ HLog.warn
+ ("There are "^string_of_int (List.length xxx + 1)^
+ " minimal joins of "^ CoercDb.string_of_carr car1^" and "^
+ CoercDb.string_of_carr car2^": " ^
+ String.concat " and "
+ (List.map
+ (fun (m2,_,c2,c2') ->
+ " via "^CoercDb.string_of_carr m2^" via "^unopt c2^" + "^unopt c2')
+ xxx))
(* NUOVA UNIFICAZIONE *)
(* A substitution is a (int * Cic.term) list that associates a
let module S = CicSubstitution in
let t1 = deref subst t1 in
let t2 = deref subst t2 in
- let b,ugraph =
+ 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
(*
(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 subst t1)
- (CicMetaSubst.ppterm subst t2))) *)
+ (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 subst t1)
- (CicMetaSubst.ppterm subst t2)))) *)
+ (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.Sort (C.Type u) when not test_equality_only ->
let u' = CicUniv.fresh () in
let s = C.Sort (C.Type u') in
- let ugraph2 =
- CicUniv.add_ge (upper u u') (lower u u') ugraph1
- in
- s,ugraph2
+ (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 *)
raise (UnificationFailure (lazy
(sprintf
"Can't unify %s with %s due to different constants"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))
+ (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
(lazy
(sprintf
"Can't unify %s with %s due to different inductive principles"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))
+ (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
(lazy
(sprintf
"Can't unify %s with %s due to different inductive constructors"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))
+ (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.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.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,t1), t2)
- | (t2, C.LetIn (_,s1,t1)) ->
+ | (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) ->
| UnificationFailure s
| Uncertain s as exn ->
(match l1, l2 with
- | (((Cic.Const (uri1, ens1)) as c1) :: tl1),
- (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
- CoercGraph.is_a_coercion c1 &&
- CoercGraph.is_a_coercion c2 &&
+ (* {{{ 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) ->
- let body1, attrs1, ugraph =
- match CicEnvironment.get_obj ugraph uri1 with
- | Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
+(*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 ?(skip_non_c=false) 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 when skip_non_c ->
+ aux c (HExtlib.list_last l)
+ (HExtlib.list_last l)
+ | 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 body2, attrs2, ugraph =
- match CicEnvironment.get_obj ugraph uri2 with
- | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
+ 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 is_composite1 =
- List.exists
- (function `Class (`Coercion _) -> true | _-> false)
- attrs1
+ 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 is_composite2 =
- List.exists
- (function `Class (`Coercion _) -> true | _-> false)
- attrs2
+ let conclude subst metasenv ugraph last_tl1' last_tl2' =
+ let subst',metasenv,ugraph =
+(*DEBUGGING ONLY:
+prerr_endline
+ ("conclude: " ^ 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
+ ("OK: "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
+ " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
+res)
+*)
in
- (match is_composite1, is_composite2 with
- | false, false -> raise exn
- | true, false ->
- let body1 = CicSubstitution.subst_vars ens1 body1 in
- let appl = Cic.Appl (body1::tl1) in
- let redappl = CicReduction.head_beta_reduce appl in
- fo_unif_subst
- test_equality_only subst context metasenv
- redappl t2 ugraph
- | false, true ->
- let body2 = CicSubstitution.subst_vars ens2 body2 in
- let appl = Cic.Appl (body2::tl2) in
- let redappl = CicReduction.head_beta_reduce appl in
- fo_unif_subst
- test_equality_only subst context metasenv
- t1 redappl ugraph
- | true, true ->
- let body1 = CicSubstitution.subst_vars ens1 body1 in
- let appl1 = Cic.Appl (body1::tl1) in
- let redappl1 = CicReduction.head_beta_reduce appl1 in
- let body2 = CicSubstitution.subst_vars ens2 body2 in
- let appl2 = Cic.Appl (body2::tl2) in
- let redappl2 = CicReduction.head_beta_reduce appl2 in
- fo_unif_subst
- test_equality_only subst context metasenv
- redappl1 redappl2 ugraph)
- (*CSC: This is necessary because of the "elim H" tactic
+(*DEBUGGING ONLY:
+prerr_endline (Printf.sprintf
+"Pullback problem\nterm1: %s\nterm2: %s\ncar1: %s\ncar2: %s\nlast_tl1: %s
+last_tl2: %s\nhead1_c: %s\nhead2_c: %s\n"
+(CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context)
+(CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context)
+(CoercDb.string_of_carr car1)
+(CoercDb.string_of_carr car2)
+(CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1 context)
+(CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2 context)
+(CoercDb.string_of_carr head1_c)
+(CoercDb.string_of_carr head2_c)
+);
+*)
+ 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
+ let _,last_tl1 =
+ inner_coerced ~skip_non_c:true (Cic.Appl l1) in
+ let _,last_tl2 =
+ inner_coerced ~skip_non_c:true (Cic.Appl l2) in
+ conclude subst metasenv ugraph last_tl1 last_tl2
+ else
+ let meets =
+ CoercGraph.meets
+ metasenv subst context (grow1,car1) (grow2,car2)
+ in
+ (match
+ HExtlib.list_findopt
+ (fun (carr,metasenv,to1,to2) meet_no ->
+ try
+ 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
+ if meet_no > 0 then
+ HLog.warn ("Using pullback number " ^ string_of_int
+ meet_no);
+ Some
+ (conclude subst metasenv ugraph last_tl1' last_tl2')
+ with
+ | UnificationFailure _
+ | Uncertain _ -> None)
+ meets
+ with
+ | Some x -> x
+ | None -> raise exn)
+ (* }}} 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
subst context metasenv t1 t2' ugraph
| _ -> raise
(UnificationFailure
- (lazy ("not a mutind :"^CicMetaSubst.ppterm subst t2 ))))
+ (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 =
raise (UnificationFailure (lazy "6.1")))
(* (sprintf
"Error trying to unify %s with %s: the number of branches is not the same."
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2)))) *)
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
| (C.Rel _, _) | (_, C.Rel _) ->
if t1 = t2 then
subst, metasenv,ugraph
raise (UnificationFailure (lazy
(sprintf
"Can't unify %s with %s because they are not convertible"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))
+ (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
subst context metasenv t1' t2 ugraph
| _ -> raise (UnificationFailure (lazy "8")))
*)
-(* The following idea could be exploited again; right now we have no
- longer any example requiring it
- | (C.Prod _, t2) ->
- let t2' = R.whd ~subst context t2 in
- (match t2' with
- C.Prod _ ->
- fo_unif_subst test_equality_only
- subst context metasenv t1 t2' ugraph
- | _ -> raise (UnificationFailure (lazy "8")))
- | (t1, C.Prod _) ->
- let t1' = R.whd ~subst context t1 in
- (match t1' with
- C.Prod _ ->
- fo_unif_subst test_equality_only
- subst context metasenv t1' t2 ugraph
- | _ -> (* raise (UnificationFailure "9")) *)
- raise
- (UnificationFailure (lazy (sprintf
- "Can't unify %s with %s because they are not convertible"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2)))))
-*)
+ | (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:
(lazy
(sprintf
"Can't unify %s with %s because they are not convertible"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))
+ (CicMetaSubst.ppterm ~metasenv subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t2))))
else
try
fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
(lazy
(sprintf
"Can't unify %s with %s because they are not convertible"
- (CicMetaSubst.ppterm subst t1)
- (CicMetaSubst.ppterm subst t2))))
+ (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
String.concat " ; "
(List.map
(fun (uri,t) ->
- UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
+ UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
) ens)
in
raise (UnificationFailure (lazy (sprintf
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 subst t1)
+ (CicMetaSubst.ppterm ~metasenv subst t1)
(try
let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
CicPp.ppterm ty_t1
| UnificationFailure s
| Uncertain s
| AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
- (CicMetaSubst.ppterm subst t2)
+ (CicMetaSubst.ppterm ~metasenv subst t2)
(try
let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
CicPp.ppterm ty_t2
| UnificationFailure s
| Uncertain s
| AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
- (CicMetaSubst.ppcontext subst context)
+ (CicMetaSubst.ppcontext ~metasenv subst context)
(CicMetaSubst.ppmetasenv subst metasenv)
- (CicMetaSubst.ppsubst subst) (Lazy.force msg)
+ (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 subst t1 context)
+ (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 subst ty_t1 context
+ 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 subst t2 context)
+ (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 subst ty_t2 context
+ 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 subst context)
- (CicMetaSubst.ppmetasenv subst metasenv)
+ (CicMetaSubst.ppcontext ~metasenv subst context)
+ ("OMITTED" (*CicMetaSubst.ppmetasenv subst metasenv*))
(Lazy.force msg)
)
projects / helm.git / blobdiff