https://github.com/EasyCrypt/easycrypt
Tip revision: 879d8424a60941bc3cb59fee3dfc02f03f193421 authored by Pierre-Yves Strub on 03 May 2020, 22:02:33 UTC
ax. for polynomials
ax. for polynomials
Tip revision: 879d842
ecUserMessages.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcSymbols
open EcUid
open EcPath
open EcUtils
open EcTypes
open EcEnv
(* -------------------------------------------------------------------- *)
type pp_options = {
ppo_prpo : EcPrinting.prpo_display;
}
let ppo : (pp_options option) ref = ref None
let set_ppo (newppo : pp_options) =
ppo := Some newppo
(* -------------------------------------------------------------------- *)
module TypingError : sig
open EcTyping
val pp_tyerror : env -> Format.formatter -> tyerror -> unit
val pp_cnv_failure : env -> Format.formatter -> tymod_cnv_failure -> unit
val pp_mismatch_funsig : env -> Format.formatter -> mismatch_funsig -> unit
val pp_modappl_error : env -> Format.formatter -> modapp_error -> unit
val pp_restr_error : env -> Format.formatter -> restriction_error -> unit
end = struct
open EcTyping
let pp_mismatch_funsig env fmt error =
let ppe = EcPrinting.PPEnv.ofenv env in
let msg x = Format.fprintf fmt x in
let pp_type fmt ty = EcPrinting.pp_type ppe fmt ty in
match error with
| MF_targs (ex, got) ->
msg "its argument has type %a instead of %a"
pp_type got pp_type ex
| MF_tres (ex, got) ->
msg "its return type is %a instead of %a"
pp_type got pp_type ex
| MF_restr (env, `Sub sx) ->
let ppe = EcPrinting.PPEnv.ofenv env in
msg "the function is not allowed to use %a"
(EcPrinting.pp_list " or@ " (EcPrinting.pp_funname ppe))
(Sx.ntr_elements sx)
| MF_restr (env, `Eq (ex, got)) ->
let ppe = EcPrinting.PPEnv.ofenv env in
let allowed = Sx.diff ex got in
let has_allowed = not (Sx.is_empty allowed) in
let notallowed = Sx.diff got ex in
if has_allowed then
msg "the function should be allowed to use %a"
(EcPrinting.pp_list " or@ " (EcPrinting.pp_funname ppe))
(Sx.ntr_elements allowed);
if not (Sx.is_empty notallowed) then
msg "%sthe function is not allowed to use %a"
(if has_allowed then ",@ " else "")
(EcPrinting.pp_list " or@ " (EcPrinting.pp_funname ppe))
(Sx.ntr_elements notallowed)
let rec pp_cnv_failure env fmt error =
let msg x = Format.fprintf fmt x in
match error with
| E_TyModCnv_ParamCountMismatch ->
msg "not the same number of module arguments"
| E_TyModCnv_ParamTypeMismatch x ->
msg "the module argument `%s' does not have the expected type"
(EcIdent.name x)
| E_TyModCnv_MissingComp x ->
msg "procedure `%s' is missing" x
| E_TyModCnv_MismatchFunSig (x,err) ->
msg "procedure `%s' is not compatible: %a"
x (pp_mismatch_funsig env) err
| E_TyModCnv_SubTypeArg(x,t1,t2,err) ->
let ppe = EcPrinting.PPEnv.ofenv env in
msg "@[<v>for argument %s:@ %a is not a subtype of %a because@ %a@]"
(EcIdent.name x)
(EcPrinting.pp_modtype1 ppe) t1
(EcPrinting.pp_modtype1 ppe) t2
(pp_cnv_failure env) err
let pp_modappl_error env fmt error =
let msg x = Format.fprintf fmt x in
match error with
| MAE_WrongArgCount (ex,got)->
msg "wrong number of arguments (expected %i, got %i)" ex got
| MAE_InvalidArgType (mp,error) ->
let ppe = EcPrinting.PPEnv.ofenv env in
msg "argument %a does not match required interface, %a"
(EcPrinting.pp_topmod ppe) mp
(pp_cnv_failure env) error
| MAE_AccesSubModFunctor ->
msg "cannot access a sub-module of a partially applied functor"
let pp_tyerror env1 fmt error =
let env = EcPrinting.PPEnv.ofenv env1 in
let msg x = Format.fprintf fmt x in
let pp_type fmt ty = EcPrinting.pp_type env fmt ty in
match error with
| UniVarNotAllowed ->
msg "type place holders not allowed"
| FreeTypeVariables ->
msg "this expression contains free type variables"
| TypeVarNotAllowed ->
msg "type variables not allowed"
| OnlyMonoTypeAllowed s ->
msg "%s, %s%a"
"only monomorphic types are allowed"
"you may have to add type annotations"
(fun fmt -> oiter (Format.fprintf fmt " on %s")) s
| UnboundTypeParameter x ->
msg "unbound type parameter: %s" x
| UnknownTypeName qs ->
msg "unknown type name: %a" pp_qsymbol qs
| UnknownTypeClass qs ->
msg "unknown type class: %a" pp_qsymbol qs
| UnknownRecFieldName qs ->
msg "unknown (record) field name: %a" pp_qsymbol qs
| UnknownInstrMetaVar x ->
msg "unkown instruction meta-variable: %a" pp_symbol x
| UnknownMetaVar x ->
msg "unknown meta-variable: %a" pp_symbol x
| DuplicatedRecFieldName qs ->
msg "duplicated (record) field name: %s" qs
| MissingRecField qs ->
msg "missing (record) field: %s" qs
| MixingRecFields (p1, p2) ->
msg "mixing (record) fields from different record types: %a / %a"
(EcPrinting.pp_tyname env) p1
(EcPrinting.pp_tyname env) p2
| UnknownProj qs ->
msg "unknown record projection: %a" pp_qsymbol qs
| AmbiguousProj qs ->
msg "ambiguous record projection: %a" pp_qsymbol qs
| AmbiguousProji (i, ty) ->
let i = max (i + 1) 2 in
msg "type %a should be a tuple of at least %i elements" pp_type ty i
| InvalidTypeAppl (name, _, _) ->
msg "invalid type application: %a" pp_qsymbol name
| DuplicatedTyVar ->
msg "a type variable appear at least twice"
| DuplicatedLocal name ->
msg "duplicated local/parameters name: `%s'" name
| DuplicatedField name ->
msg "duplicated field name: `%s'" name
| NonLinearPattern ->
msg "non-linear pattern matching"
| LvNonLinear ->
msg "This left-value is contains twice the same variable"
| NonUnitFunWithoutReturn ->
msg "This function must return a value"
| TypeMismatch ((ty1, ty2), _) ->
msg "This expression has type@\n";
msg " @[<hov 2> %a@]@\n@\n" pp_type ty2;
msg "but is expected to have type@\n";
msg " @[<hov 2> %a@]" pp_type ty1
| TypeClassMismatch ->
msg "Type-class unification failure"
| TypeModMismatch(mp, mt, err) ->
msg "the module %a does not have the module type %a:@\n"
(EcPrinting.pp_topmod env) mp
(EcPrinting.pp_modtype1 env) mt;
msg " @[<hov 2>%t@]" (fun fmt -> pp_cnv_failure env1 fmt err)
| NotAFunction ->
msg "the expression is not a function, it can not be applied"
| AbbrevLowArgs ->
msg "this abbreviation is not applied enough"
| UnknownProgVar (p, mem) ->
msg "unknown program variable (in %a): `%a'"
(EcPrinting.pp_mem env) mem pp_qsymbol p
| UnknownVarOrOp (name, []) ->
msg "unknown variable or constant: `%a'" pp_qsymbol name
| UnknownVarOrOp (name, tys) ->
msg "no matching operator, named `%a', " pp_qsymbol name;
msg "for the following parameters' type:@\n";
List.iteri (fun i ty -> msg " [%d]: @[%a@]@\n" (i+1) pp_type ty) tys
| MultipleOpMatch (name, tys, matches) -> begin
let uvars = List.map EcTypes.Tuni.univars tys in
let uvars = List.fold_left Suid.union Suid.empty uvars in
begin match tys with
| [] ->
msg
"more that one variable or constant matches `%a'@\n"
pp_qsymbol name
| _ ->
let pp_argty i ty = msg " [%d]: @[%a@]@\n" (i+1) pp_type ty in
msg "more than one operator, named `%a', matches.@\n@\n" pp_qsymbol name;
msg "operator parameters' type were:@\n";
List.iteri pp_argty tys
end;
msg "@\n";
let pp_op fmt ((op, inst), subue) =
let inst = Tuni.offun_dom (EcUnify.UniEnv.assubst subue) inst in
begin match inst with
| [] ->
Format.fprintf fmt "%a"
EcPrinting.pp_path op
| _ ->
Format.fprintf fmt "%a <%a>"
EcPrinting.pp_path op
(EcPrinting.pp_list ",@ " pp_type) inst
end;
let myuvars = List.map EcTypes.Tuni.univars inst in
let myuvars = List.fold_left Suid.union uvars myuvars in
let myuvars = Suid.elements myuvars in
let tysubst = Tuni.offun (EcUnify.UniEnv.assubst subue) in
let myuvars = List.pmap
(fun uid ->
match tysubst (tuni uid) with
| { ty_node = Tunivar uid' } when uid = uid' -> None
| ty -> Some (uid, ty))
myuvars
in
if not (List.is_empty myuvars) then begin
Format.fprintf fmt "@\n where@\n";
List.iter (fun (uid, uidty) ->
Format.fprintf fmt " %a = %a@\n"
(EcPrinting.pp_tyunivar env) uid pp_type uidty)
myuvars
end
in
msg "the list of matching objects follows:@\n";
List.iter (fun (m, ue) ->
let (title, Cb (x, pp)) =
match m with
| `Var pv ->
("prog. variable", Cb (pv, EcPrinting.pp_pv env))
| `Lc id ->
("local variable", Cb (id, EcPrinting.pp_local env))
| `Proj (pv, _, _) ->
("variable proj.", Cb (pv, EcPrinting.pp_pv env))
| `Op op ->
("operator", Cb ((op, ue), pp_op))
in msg " [%s]: %a@\n" title pp x) matches
end
| UnknownModName name ->
msg "unknown module: %a" pp_qsymbol name
| UnknownTyModName name ->
msg "unknown type name: %a" pp_qsymbol name
| UnknownFunName name ->
msg "unknown function: %a" pp_qsymbol name
| UnknownModVar x ->
msg "unknown module-level variable: %a" pp_qsymbol x
| UnknownMemName m ->
msg "unknown memory: %s" m
| InvalidFunAppl FAE_WrongArgCount ->
msg "invalid function application: wrong number of arguments"
| InvalidModAppl err ->
msg "invalid module application:@ %a" (pp_modappl_error env1) err
| InvalidModType MTE_IncludeFunctor ->
msg "cannot include functors"
| InvalidModType MTE_InnerFunctor ->
msg "functors must be top-level modules"
| InvalidModType (MTE_DupProcName x) ->
msg "duplicated var/proc name in module expression: `%s'" x
| InvalidModSig (MTS_DupProcName x) ->
msg "duplicated proc. name in signature: `%s'" x
| InvalidModSig (MTS_DupArgName (f, x)) ->
msg "duplicated proc. arg. name in signature: `%s.%s'" f x
| InvalidMem (name, MAE_IsConcrete) ->
msg "the memory %s must be abstract" name
| InvalidFilter (FE_InvalidIndex i) ->
msg "invalid filter index: %d" i
| InvalidFilter FE_NoMatch ->
msg "invalid filter pattern (no match)"
| FunNotInModParam name ->
msg "the function %a is not provided by a module parameter"
pp_qsymbol name
| NoActiveMemory ->
msg "no active memory at this point"
| PatternNotAllowed ->
msg "pattern not allowed here"
| MemNotAllowed ->
msg "memory not allowed here"
| UnknownScope sc ->
msg "unknown scope: `%a'" pp_qsymbol sc
| FilterMatchFailure ->
msg "filter pattern does not match"
let pp_restr_error env fmt (w, e) =
let ppe = EcPrinting.PPEnv.ofenv env in
let pp_v fmt xp = EcPrinting.pp_pv ppe fmt (pv_glob xp) in
let pp_m fmt m = EcPrinting.pp_topmod ppe fmt m in
let pp_restriction_who fmt = function
| RW_mod mp ->
Format.fprintf fmt "the module %a" pp_m mp
| RW_fun xp ->
Format.fprintf fmt "the procedure %a" (EcPrinting.pp_funname ppe) xp in
let pp_restriction_err fmt = function
| RE_UseVariable x ->
Format.fprintf fmt
"should not be able to use the variable %a"
pp_v x
| RE_UseVariableViaModule (x, m) ->
Format.fprintf fmt
"should not be able to use %a (via %a)"
pp_v x pp_m m
| RE_UseModule m ->
Format.fprintf fmt
"should not be able to use the module %a"
pp_m m
| RE_VMissingRestriction (x, (m1, m2))->
Format.fprintf fmt
"should not be able to use %a, add restriction %a to %a"
pp_v x pp_m m1 pp_m m2
| RE_MMissingRestriction (m, (m1, m2))->
Format.fprintf fmt
"should not be able to use %a, add restriction %a to %a or %a to %a"
pp_m m pp_m m1 pp_m m2 pp_m m2 pp_m m1
in Format.fprintf fmt "%a %a" pp_restriction_who w pp_restriction_err e
end
(* -------------------------------------------------------------------- *)
module InductiveError : sig
open EcHiInductive
val pp_rcerror : env -> Format.formatter -> rcerror -> unit
val pp_dterror : env -> Format.formatter -> dterror -> unit
val pp_fxerror : env -> Format.formatter -> fxerror -> unit
end = struct
open EcHiInductive
open TypingError
let pp_rcerror env fmt error =
let msg x = Format.fprintf fmt x in
match error with
| RCE_TypeError ee ->
pp_tyerror env fmt ee
| RCE_DuplicatedField name ->
msg "duplicated field: `%s'" name
| RCE_InvalidFieldType (name, ee) ->
msg "invalid field type: `%s`: %a'" name (pp_tyerror env) ee
| RCE_Empty ->
msg "this record type is empty"
let pp_dterror env fmt error =
let msg x = Format.fprintf fmt x in
match error with
| DTE_TypeError ee ->
pp_tyerror env fmt ee
| DTE_DuplicatedCtor name ->
msg "duplicated constructor name: `%s'" name
| DTE_InvalidCTorType (name, ee) ->
msg "invalid constructor type: `%s`: %a'"
name (pp_tyerror env) ee
| DTE_NonPositive ->
msg "the datatype does not respect the positivity condition"
| DTE_Empty ->
msg "the datatype may be empty"
let pp_fxerror env fmt error =
let msg x = Format.fprintf fmt x in
match error with
| FXE_TypeError ee ->
pp_tyerror env fmt ee
| FXE_EmptyMatch ->
msg "this pattern matching has no branches"
| FXE_MatchParamsMixed ->
msg "this pattern matching matches on different parameters"
| FXE_MatchParamsDup ->
msg "this pattern matching matches a parameter twice"
| FXE_MatchParamsUnk ->
msg "this pattern matching matches an unbound parameter"
| FXE_MatchNonLinear ->
msg "this pattern is non-linear"
| FXE_MatchDupBranches ->
msg "this pattern matching contains duplicated branches"
| FXE_MatchPartial ->
msg "this pattern matching is non-exhaustive"
| FXE_CtorUnk ->
msg "unknown constructor name"
| FXE_CtorAmbiguous ->
msg "ambiguous constructor name"
| FXE_CtorInvalidArity (cname, i, j) ->
msg
"the constructor %s expects %d argument(s) (%d argument(s) given)"
cname i j
end
(* -------------------------------------------------------------------- *)
module PredError : sig
open EcHiPredicates
val pp_tperror : env -> Format.formatter -> tperror -> unit
end = struct
open EcHiPredicates
let pp_tperror (env : env) fmt = function
| TPE_Typing e ->
TypingError.pp_tyerror env fmt e
| TPE_TyNotClosed ->
Format.fprintf fmt "this predicate type contains free type variables"
| TPE_DuplicatedConstr x ->
Format.fprintf fmt "duplicated constructor name: `%s'" x
end
(* -------------------------------------------------------------------- *)
module NotationsError : sig
open EcHiNotations
val pp_nterror : env -> Format.formatter -> nterror -> unit
end = struct
open EcHiNotations
let pp_nterror (env : env) fmt error =
let msg x = Format.fprintf fmt x in
match error with
| NTE_Typing e ->
TypingError.pp_tyerror env fmt e
| NTE_TyNotClosed ->
msg "this notation type contains free type variables"
| NTE_DupIdent ->
msg "an ident is bound several time"
| NTE_UnknownBinder x ->
msg "unknown binder: `%s'" x
| NTE_AbbrevIsVar ->
msg "abbrev. body cannot reduce to a variable"
end
(* -------------------------------------------------------------------- *)
module CloneError : sig
open EcThCloning
val string_of_ovkind : ovkind -> string
val pp_clone_error : env -> Format.formatter -> clone_error -> unit
end = struct
open EcThCloning
let string_of_ovkind = function
| OVK_Type -> "type"
| OVK_Operator -> "operator"
| OVK_Predicate -> "predicate"
| OVK_Theory -> "theory"
| OVK_Lemma -> "lemma/axiom"
let pp_incompatible env fmt = function
| NotSameNumberOfTyParam (exp, got) ->
Format.fprintf fmt "contains %i type parameter instead of %i" got exp
| DifferentType (exp, got) ->
let ppe = EcPrinting.PPEnv.ofenv env in
Format.fprintf fmt "has type %a instead of %a"
(EcPrinting.pp_type ppe) got (EcPrinting.pp_type ppe) exp
let pp_clone_error env fmt error =
let msg x = Format.fprintf fmt x in
match error with
| CE_UnkTheory name ->
msg "cannot find theory to clone: `%s'"
(string_of_qsymbol name)
| CE_DupOverride (kd, x) ->
msg "the %s `%s' is instantiate twice"
(string_of_ovkind kd) (string_of_qsymbol x)
| CE_UnkOverride (kd, x) ->
msg "unknown %s `%s'"
(string_of_ovkind kd) (string_of_qsymbol x)
| CE_CrtOverride (kd, x) ->
msg "cannot instantiate the _concrete_ %s `%s' / they may be not convertible"
(string_of_ovkind kd) (string_of_qsymbol x)
| CE_UnkAbbrev x ->
msg "unknown abbreviation: `%s'" (string_of_qsymbol x)
| CE_TypeArgMism (kd, x) ->
msg "type argument mismatch for %s `%s'"
(string_of_ovkind kd) (string_of_qsymbol x)
| CE_OpIncompatible (x, err) ->
msg "operator `%s' body %a"
(string_of_qsymbol x) (pp_incompatible env) err
| CE_PrIncompatible (x, err) ->
msg "predicate `%s' body %a"
(string_of_qsymbol x) (pp_incompatible env) err
| CE_InvalidRE x ->
msg "invalid regexp: `%s'" x
end
(* -------------------------------------------------------------------- *)
module PTermError : sig
open EcProofTerm
val string_of_argkind : argkind -> string
val pp_pterm_apperror : Format.formatter -> pterror -> unit
end = struct
open EcProofTerm
open TypingError
let string_of_argkind (ak : argkind) =
match ak with
| `Form -> "formula"
| `Mem -> "memory"
| `Mod -> "module"
| `PTerm -> "proof-term"
let pp_pterm_apperror fmt (((hyps, ue, ev), kind) : pterror) =
let msg x = Format.fprintf fmt x in
match kind with
| AE_WrongArgKind (src, dst) ->
msg "expecting a `%s', not a `%s'"
(string_of_argkind dst) (string_of_argkind src)
| AE_CannotInfer -> msg "%s" "cannot infer this place-holder"
| AE_CannotInferMod -> msg "%s" "cannot infer module arguments"
| AE_NotFunctional -> msg "%s" "too many argument"
| AE_InvalidArgForm (IAF_Mismatch (src, dst)) ->
let ppe = EcPrinting.PPEnv.ofenv (LDecl.toenv hyps) in
let dst = Tuni.offun (EcUnify.UniEnv.assubst ue) dst in
msg "This expression has type@\n";
msg " @[<hov 2>%a@]@\n@\n" (EcPrinting.pp_type ppe) src;
msg "but is expected to have type@\n";
msg " @[<hov 2>%a@]" (EcPrinting.pp_type ppe) dst
| AE_InvalidArgForm (IAF_TyError (env, err)) ->
msg "This proof-term argument is not a valid formula:@\n@\n";
msg " @[<hov 2>%a@]@\n" (pp_tyerror env) err
| AE_InvalidArgMod ->
msg "%s" "invalid argument (incompatible module type)"
| AE_InvalidArgProof (src, dst) ->
let ppe = EcPrinting.PPEnv.ofenv (LDecl.toenv hyps) in
let sb = EcMatching.CPTEnv (EcMatching.MEV.assubst ue ev) in
let src = concretize_e_form sb src in
let dst = concretize_e_form sb dst in
msg "this proof-term proves:@\n@\n";
msg " @[<hov 2>%a@]@\n@\n" (EcPrinting.pp_form ppe) src;
msg "but is expected to prove:@\n@\n";
msg " @[<hov 2>%a@]@\n" (EcPrinting.pp_form ppe) dst
| AE_InvalidArgModRestr e ->
msg "%a" (pp_restr_error (LDecl.toenv hyps)) e
end
(* -------------------------------------------------------------------- *)
let pp_apply_error fmt (dpe, reason, pt, (src, dst)) =
let module PT = EcProofTerm in
let ppe = EcPrinting.PPEnv.ofenv (LDecl.toenv pt.PT.pte_hy) in
let src = PT.concretize_form pt src in
Format.fprintf fmt "the given proof-term proves:@\n@\n";
Format.fprintf fmt " @[%a@]@\n@\n" (EcPrinting.pp_form ppe) src;
match reason with
| `DoNotMatch ->
Format.fprintf fmt "it does not apply to the goal@\n@\n";
if dpe then begin
Format.fprintf fmt " @[%a@]@\n@\n" (EcPrinting.pp_form ppe) dst
end;
| `IncompleteInference ->
Format.fprintf fmt "not all variables can be inferred@\n"
(* -------------------------------------------------------------------- *)
let pp_parse_error fmt msg =
match msg with
| Some msg -> Format.fprintf fmt "parse error: %s" msg
| None -> Format.fprintf fmt "parse error"
(* -------------------------------------------------------------------- *)
let pp_alias_clash env fmt = function
| EcPV.AC_concrete_abstract (mp, npv) ->
let top = m_functor npv.pv_name.x_top in
let ppe = EcPrinting.PPEnv.ofenv env in
Format.fprintf fmt
"The module %a can write %a (maybe add restriction %a)"
(EcPrinting.pp_topmod ppe) mp
(EcPrinting.pp_pv ppe) npv
(EcPrinting.pp_topmod ppe) top
| EcPV.AC_abstract_abstract (mp, mp') ->
let ppe = EcPrinting.PPEnv.ofenv env in
Format.fprintf fmt
"The module %a can write %a (add restriction %a to %a, or %a to %a)"
(EcPrinting.pp_topmod ppe) mp
(EcPrinting.pp_topmod ppe) mp'
(EcPrinting.pp_topmod ppe) mp
(EcPrinting.pp_topmod ppe) mp'
(EcPrinting.pp_topmod ppe) mp'
(EcPrinting.pp_topmod ppe) mp
(* -------------------------------------------------------------------- *)
module RedError : sig
open EcFol
val pp_incompatible_form : Format.formatter -> env -> form pair -> unit
val pp_incompatible_type : Format.formatter -> env -> ty pair -> unit
end = struct
module PE = EcPrinting
let pp_incompatible_form fmt env (f1, f2) =
Format.fprintf fmt
"the formula %a is not compatible with %a\n%!"
(PE.pp_form (PE.PPEnv.ofenv env)) f1
(PE.pp_form (PE.PPEnv.ofenv env)) f2
let pp_incompatible_type fmt env (t1, t2) =
Format.fprintf fmt
"the type %a is not compatible with %a\n%!"
(PE.pp_type (PE.PPEnv.ofenv env)) t1
(PE.pp_type (PE.PPEnv.ofenv env)) t2
end
(* -------------------------------------------------------------------- *)
let pp_tc_error fmt error =
let module G = EcCoreGoal in
let pname, penv =
match error.G.tc_reloced with
| Some (name, ppgoal) ->
(Some name, if ppgoal then error.G.tc_proofenv else None)
| None -> (None, None)
in
let pp_penv penv =
let goal = G.FApi.get_main_pregoal penv in
let ppe = EcPrinting.PPEnv.ofenv (LDecl.toenv goal.G.g_hyps) in
Format.fprintf fmt "\nInitial goal was:\n\n%!";
Format.fprintf fmt "%a\n%!"
(EcPrinting.pp_goal ppe (oget !ppo).ppo_prpo)
((LDecl.tohyps goal.G.g_hyps, goal.G.g_concl), `One (-1))
in
pname |> oiter (Format.fprintf fmt "In proving `%s':\n\n%!");
(match error.G.tc_message with
| G.TCEUser (x, f) ->
Format.fprintf fmt "%s\n%!" (f x)
| G.TCEExn e ->
Format.fprintf fmt "%a" EcPException.exn_printer e);
penv |> oiter pp_penv
(* -------------------------------------------------------------------- *)
let pp_error_clear fmt err =
let pp_id fmt id = Format.fprintf fmt "%s" (EcIdent.name id) in
match Lazy.force err with
| `ClearInGoal xs ->
Format.fprintf fmt
"cannot clear %a that is/are used in the conclusion"
(EcPrinting.pp_list ",@ " pp_id) xs
| `ClearDep (x, y) ->
Format.fprintf fmt
"cannot clear %a that is used in %a"
pp_id x pp_id y
(* -------------------------------------------------------------------- *)
let pp fmt exn =
match exn with
| EcHiInductive.RcError (_, env, e) -> InductiveError.pp_rcerror env fmt e
| EcHiInductive.DtError (_, env, e) -> InductiveError.pp_dterror env fmt e
| EcHiInductive.FxError (_, env, e) -> InductiveError.pp_fxerror env fmt e
| EcHiPredicates.TransPredError (_, env, e) ->
PredError.pp_tperror env fmt e
| EcHiNotations.NotationError (_, env, e) ->
NotationsError.pp_nterror env fmt e
| EcPV.AliasClash (env, ac) ->
pp_alias_clash env fmt ac
| EcThCloning.CloneError (env, e) ->
CloneError.pp_clone_error env fmt e
| EcCoreGoal.TcError error ->
pp_tc_error fmt error
| EcParsetree.ParseError (_loc, msg) ->
pp_parse_error fmt msg
| EcReduction.IncompatibleForm (env, (f1, f2)) ->
RedError.pp_incompatible_form fmt env (f1, f2)
| EcReduction.IncompatibleType (env, (t1, t2)) ->
RedError.pp_incompatible_type fmt env (t1, t2)
| EcTyping.TyError (_, env, e) ->
TypingError.pp_tyerror env fmt e
| EcTyping.RestrictionError (env, e) ->
TypingError.pp_restr_error env fmt e
| EcProofTerm.ProofTermError e ->
PTermError.pp_pterm_apperror fmt e
| EcCoreGoal.ClearError e ->
pp_error_clear fmt e
| EcLowGoal.Apply.NoInstance e ->
pp_apply_error fmt e
| _ -> raise exn
(* -------------------------------------------------------------------- *)
let register =
let first = ref true in fun () ->
if !first then EcPException.register pp; first := false