Quelle himsg.ml Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Pp
open Util
open Names
open Nameops
open Namegen
open Constr
open Context
open Termops
open Environ
open Pretype_errors
open Type_errors
open Typeclasses_errors
open Indrec
open Cases
open Logic
open Printer
open Evd
open Context.Rel.Declaration

module RelDecl = Context.Rel.Declaration

(* This simplifies the typing context of Cases clauses *)
(* hope it does not disturb other typing contexts *)
let contract env sigma lc =
  let open EConstr in
  let l = ref [] in
  let contract_context decl env =
    match decl with
      | LocalDef (_,c',_) when isRel sigma c' ->
          l := (Vars.substl !l c') :: !l;
          env
      | _ ->
          let t = Vars.substl !l (RelDecl.get_type decl) in
          let decl = decl |> RelDecl.map_name (named_hd env sigma t) |> RelDecl.map_value (Vars.substl !l) |> RelDecl.set_type t in
          l := (mkRel 1) :: List.map (Vars.lift 1) !l;
          push_rel decl env
  in
  let env = process_rel_context contract_context env in
  (env, List.map (Vars.substl !l) lc)

let contract2 env sigma a b = match contract env sigma [a;b] with
  | env, [a;b] -> env,a,b | _ -> assert false

let contract3 env sigma a b c = match contract env sigma [a;b;c] with
  | env, [a;b;c] -> env,a,b,c | _ -> assert false

let contract4 env sigma a b c d = match contract env sigma [a;b;c;d] with
  | env, [a;b;c;d] -> (env,a,b,c),d | _ -> assert false

let contract1 env sigma a v =
  match contract env sigma (a :: v) with
  | env, a::l -> env,a,l
  | _ -> assert false

let rec contract3' env sigma a b c = function
  | OccurCheck (evk,d) ->
    let x,d = contract4 env sigma a b c d in x,OccurCheck(evk, d)
  | NotClean ((evk,args),env',d) ->
      let args = Evd.expand_existential sigma (evk, args) in
      let env',d,args = contract1 env' sigma d args in
      let args = SList.of_full_list args in
      contract3 env sigma a b c,NotClean((evk,args),env',d)
  | ConversionFailed (env',t1,t2) ->
      let (env',t1,t2) = contract2 env' sigma t1 t2 in
      contract3 env sigma a b c, ConversionFailed (env',t1,t2)
  | IncompatibleInstances (env',ev,t1,t2) ->
      let (env',ev,t1,t2) = contract3 env' sigma (EConstr.mkEvar ev) t1 t2 in
      contract3 env sigma a b c, IncompatibleInstances (env',EConstr.destEvar sigma ev,t1,t2)
  | NotSameArgSize | NotSameHead | NoCanonicalStructure | MetaOccurInBody _
  | InstanceNotSameType _ | InstanceNotFunctionalType _ | ProblemBeyondCapabilities
  | UnifUnivInconsistency _ as x -> contract3 env sigma a b c, x
  | CannotSolveConstraint ((pb,env',t,u),x) ->
      let env',t,u = contract2 env' sigma t u in
      let y,x = contract3' env sigma a b c x in
      y,CannotSolveConstraint ((pb,env',t,u),x)

(** Ad-hoc reductions *)

let j_nf_betaiotaevar env sigma j =
  { uj_val = j.uj_val;
    uj_type = Reductionops.nf_betaiota env sigma j.uj_type }

let jv_nf_betaiotaevar env sigma jl =
  Array.Smart.map (fun j -> j_nf_betaiotaevar env sigma j) jl

(** Printers *)

let pr_lconstr_env e s c = quote (pr_lconstr_env e s c)
let pr_leconstr_env e s c = quote (pr_leconstr_env e s c)
let pr_ljudge_env e s c = let v,t = pr_ljudge_env e s c in (quote v,quote t)

(** A canonisation procedure for constr such that comparing there
    externalisation catches more equalities *)
let canonize_constr sigma c =
  (* replaces all the names in binders by [dn] ("default name"),
     ensures that [alpha]-equivalent terms will have the same
     externalisation. *)
  let open EConstr in
  let dn = Name.Anonymous in
  let rec canonize_binders c =
    match EConstr.kind sigma c with
    | Prod (x,t,b) -> mkProd({x with binder_name=dn},t,b)
    | Lambda (x,t,b) -> mkLambda({x with binder_name=dn},t,b)
    | LetIn (x,u,t,b) -> mkLetIn({x with binder_name=dn},u,t,b)
    | _ -> EConstr.map sigma canonize_binders c
  in
  canonize_binders c

let rec display_expr_eq c1 c2 =
  let open Constrexpr in
  match CAst.(c1.v, c2.v) with
  | (CHole _ | CEvar _), _ | _, (CEvar _ | CHole _) -> true
  | _ ->
    Constrexpr_ops.constr_expr_eq_gen display_expr_eq c1 c2

let safe_extern_constr env sigma t =
  Printer.safe_extern_wrapper begin fun env sigma () ->
    Constrextern.extern_constr env sigma t
  end env sigma ()

(** Tries to realize when the two terms, albeit different are printed the same. *)
let display_eq ~flags env sigma t1 t2 =
  (* terms are canonized, then their externalisation is compared syntactically *)
  let t1 = canonize_constr sigma t1 in
  let t2 = canonize_constr sigma t2 in
  let ct1 = Flags.with_options flags (fun () -> safe_extern_constr env sigma t1) () in
  let ct2 = Flags.with_options flags (fun () -> safe_extern_constr env sigma t2) () in
  match ct1, ct2 with
  | None, None -> false
  | Some _, None | None, Some _ -> false
  | Some ct1, Some ct2 -> display_expr_eq ct1 ct2

(** This function adds some explicit printing flags if the two arguments are
    printed alike. *)
let rec pr_explicit_aux env sigma t1 t2 = function
| [] ->
  (* no specified flags: default. *)
  Printer.pr_leconstr_env env sigma t1, Printer.pr_leconstr_env env sigma t2
| flags :: rem ->
  let equal = display_eq ~flags env sigma t1 t2 in
  if equal then
    (* The two terms are the same from the user point of view *)
    pr_explicit_aux env sigma t1 t2 rem
  else
    let ct1 = Flags.with_options flags (fun () -> safe_extern_constr env sigma t1) () in
    let ct2 = Flags.with_options flags (fun () -> safe_extern_constr env sigma t2) () in
    let pr = function
    | None -> str "??"
    | Some c -> Ppconstr.pr_lconstr_expr env sigma c
    in
    pr ct1, pr ct2

let explicit_flags =
  let open Constrextern in
  [ []; (* First, try with the current flags *)
    [print_implicits]; (* Then with implicit *)
    [print_universes]; (* Then with universes *)
    [print_universes; print_implicits]; (* With universes AND implicits *)
    [print_implicits; print_coercions; print_no_symbol]; (* Then more! *)
    [print_universes; print_implicits; print_coercions; print_no_symbol] (* and more! *) ]

let with_diffs pm pn =
  if not (Proof_diffs.show_diffs ()) then pm, pn else
  try
    let tokenize_string = Proof_diffs.tokenize_string in
    Pp_diff.diff_pp ~tokenize_string pm pn
  with Pp_diff.Diff_Failure msg ->
    begin
      try ignore(Sys.getenv("HIDEDIFFFAILUREMSG"))
      with Not_found -> Proof_diffs.notify_proof_diff_failure msg
    end;
    pm, pn

let pr_explicit env sigma t1 t2 =
  let p1, p2 = pr_explicit_aux env sigma t1 t2 explicit_flags in
  let p1, p2 = with_diffs p1 p2 in
  quote p1, quote p2

let pr_db env i =
  try
    match env |> lookup_rel i |> get_name with
      | Name id -> Id.print id
      | Anonymous -> str "<>"
  with Not_found -> str "UNBOUND_REL_" ++ int i

let explain_unbound_rel env sigma n =
  let pe = pr_ne_context_of (str "In environment") env sigma in
  str "Unbound reference: " ++ pe ++
  str "The reference " ++ int n ++ str " is free."

let explain_unbound_var env v =
  let var = Id.print v in
  str "No such section variable or assumption: " ++ var ++ str "."

let explain_not_type env sigma j =
  let pe = pr_ne_context_of (str "In environment") env sigma in
  let pc,pt = pr_ljudge_env env sigma j in
  pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++
  str "has type" ++ spc () ++ pt ++ spc () ++
  str "which should be Set, Prop or Type."

let explain_bad_assumption env sigma j =
  let pe = pr_ne_context_of (str "In environment") env sigma in
  let pc,pt = pr_ljudge_env env sigma j in
  pe ++ str "Cannot declare a variable or hypothesis over the term" ++
  brk(1,1) ++ pc ++ spc () ++ str "of type" ++ spc () ++ pt ++ spc () ++
  str "because this term is not a type."

let explain_reference_variables sigma id c =
  pr_global c ++ strbrk " depends on the variable " ++ Id.print id ++
  strbrk " which is not declared in the context."

let explain_elim_arity env sigma ind c okinds =
  let open EConstr in
  let env = make_all_name_different env sigma in
  let mib, mip as specif = Inductive.lookup_mind_specif env (fst ind) in
  let pi =
    let pp () = pr_pinductive env sigma ind in
    match mip.mind_squashed with
    | None | Some AlwaysSquashed -> pp ()
    | Some (SometimesSquashed _) ->
      (* universe instance matters, so print it regardless of Printing Universes *)
      Flags.with_option Constrextern.print_universes pp ()
  in
  let pc = Option.map (pr_leconstr_env env sigma) c in
  let msg = match okinds with
    | None -> str "ill-formed elimination predicate."
    | Some sp ->
      let ppt ?(ppunivs=false) () =
        let pp () = pr_leconstr_env env sigma (mkSort (ESorts.make sp)) in
        if ppunivs then Flags.with_option Constrextern.print_universes pp ()
        else pp ()
      in
      let squash = Option.get (Inductive.is_squashed (specif, snd ind)) in
      match squash with
      | SquashToSet ->
        let ppt = ppt () in
        hov 0
          (str "the return type has sort" ++ spc () ++ ppt ++ spc () ++
           str "while it should be SProp, Prop or Set.") ++
        fnl () ++
        hov 0
          (str "Elimination of an inductive object of sort Set" ++ spc() ++
           str "is not allowed on a predicate in sort " ++ ppt ++ fnl () ++
           str "because" ++ spc () ++
           str "strong elimination on non-small inductive types leads to paradoxes.")
      | SquashToQuality (QConstant (QSProp | QProp as squashq)) ->
        let ppt = ppt () in
        let inds, sorts, explain = match squashq with
          | QSProp -> "SProp", "SProp", "strict proofs can be eliminated only to build strict proofs"
          | QProp -> "Prop", "SProp or Prop", "proofs can be eliminated only to build proofs"
          | QType -> assert false
        in
        hov 0
          (str "the return type has sort" ++ spc () ++ ppt ++ spc () ++
           str "while it should be " ++ str sorts ++ str ".") ++
        fnl () ++
        hov 0
          (str "Elimination of an inductive object of sort " ++ str inds ++ spc() ++
           str "is not allowed on a predicate in sort " ++ ppt ++ fnl () ++
           str "because" ++ spc () ++
           str explain ++ str ".")
      | SquashToQuality (QConstant QType) ->
        let ppt = ppt ~ppunivs:true () in
        hov 0
          (str "the return type has sort" ++ spc () ++ ppt ++ spc () ++
           str "while it may not be of a variable sort quality.") ++
        fnl () ++
        hov 0
          (str "Elimination of a sort polymorphic inductive object instantiated to sort Type" ++ spc() ++
           (* NB: this restriction is only for forward compat with possible future sort qualities *)
           str "is not allowed on a predicate in a variable sort quality.")
      | SquashToQuality (QVar squashq) ->
        let ppt = ppt ~ppunivs:true () in
        hov 0
          (str "the return type has sort" ++ spc () ++ ppt ++ spc () ++
           str "while it should be in sort quality " ++ pr_evd_qvar sigma squashq ++ str ".") ++
        fnl () ++
        hov 0
          (str "Elimination of a sort polymorphic inductive object instantiated to a variable sort quality" ++ spc() ++
           str "is only allowed on a predicate in the same sort quality.")
  in
  hov 0 (
    str "Incorrect elimination" ++
    (match pc with None -> mt() | Some pc -> str " of" ++ spc () ++ pc) ++ spc () ++
    str "in the inductive type" ++ spc () ++ quote pi ++ str ":") ++
  fnl () ++ msg

let explain_case_not_inductive env sigma cj =
  let env = make_all_name_different env sigma in
  let pc = pr_leconstr_env env sigma cj.uj_val in
  let pct = pr_leconstr_env env sigma cj.uj_type in
    match EConstr.kind sigma cj.uj_type with
      | Evar _ ->
          str "Cannot infer a type for this expression."
      | _ ->
          str "The term" ++ brk(1,1) ++ pc ++ spc () ++
          str "has type" ++ brk(1,1) ++ pct ++ spc () ++
          str "which is not a (co-)inductive type."

let explain_case_on_private_ind env sigma ind =
  str "Case analysis on private inductive "++pr_inductive env ind

let explain_number_branches env sigma cj expn =
  let env = make_all_name_different env sigma in
  let pc = pr_leconstr_env env sigma cj.uj_val in
  let pct = pr_leconstr_env env sigma cj.uj_type in
  str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++
  str "of type" ++ brk(1,1) ++ pct ++ spc () ++
  str "expects " ++  int expn ++ str " branches."

let explain_ill_formed_case_params env sigma =
  str "Ill formed case parameters (bugged tactic?)."

let explain_ill_formed_branch env sigma c ci actty expty =
  let simp t = Reductionops.nf_betaiota env sigma t in
  let env = make_all_name_different env sigma in
  let pc = pr_leconstr_env env sigma c in
  let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in
  strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++
  spc () ++ strbrk "the branch for constructor" ++ spc () ++
  quote (pr_pconstructor env sigma ci) ++
  spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++
  str "which should be" ++ brk(1,1) ++ pe ++ str "."

let explain_generalization env sigma (name,var) j =
  let pe = pr_ne_context_of (str "In environment") env sigma in
  let pv = pr_letype_env env sigma var in
  let (pc,pt) = pr_ljudge_env (push_rel_assum (make_annot name EConstr.ERelevance.relevant,var) env) sigma j in
  pe ++ str "Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
  str "over" ++ brk(1,1) ++ pc ++ str "," ++ spc () ++
  str "it has type" ++ spc () ++ pt ++
  spc () ++ str "which should be Set, Prop or Type."

let explain_unification_error env sigma p1 p2 = function
  | None -> mt()
  | Some e ->
     let rec aux p1 p2 = function
     | OccurCheck (evk,rhs) ->
        [str "cannot define " ++ quote (pr_existential_key env sigma evk) ++
        strbrk " with term " ++ pr_leconstr_env env sigma rhs ++
        strbrk " that would depend on itself"]
     | NotClean ((evk,args),env,c) ->
        let args = Evd.expand_existential sigma (evk, args) in
        let env = make_all_name_different env sigma in
        [str "cannot instantiate " ++ quote (pr_existential_key env sigma evk)
        ++ strbrk " because " ++ pr_leconstr_env env sigma c ++
        strbrk " is not in its scope" ++
        (if List.is_empty args then mt() else
         strbrk ": available arguments are " ++
         pr_sequence (pr_leconstr_env env sigma) (List.rev args))]
     | NotSameArgSize | NotSameHead | NoCanonicalStructure ->
        (* Error speaks from itself *) []
     | ConversionFailed (env,t1,t2) ->
        let t1 = Reductionops.nf_betaiota env sigma t1 in
        let t2 = Reductionops.nf_betaiota env sigma t2 in
        if EConstr.eq_constr sigma t1 p1 && EConstr.eq_constr sigma t2 p2 then [] else
        let env = make_all_name_different env sigma in
        if not (EConstr.eq_constr sigma t1 p1) || not (EConstr.eq_constr sigma t2 p2) then
          let t1, t2 = pr_explicit env sigma t1 t2 in
          [str "cannot unify " ++ t1 ++ strbrk " and " ++ t2]
        else []
     | IncompatibleInstances (env,ev,t1,t2) ->
        let env = make_all_name_different env sigma in
        let ev = pr_leconstr_env env sigma (EConstr.mkEvar ev) in
        let t1 = Reductionops.nf_betaiota env sigma t1 in
        let t2 = Reductionops.nf_betaiota env sigma t2 in
        let t1, t2 = pr_explicit env sigma t1 t2 in
        [ev ++ strbrk " has otherwise to unify with " ++ t1 ++ str " which is incompatible with " ++ t2]
     | MetaOccurInBody evk ->
        [str "instance for " ++ quote (pr_existential_key env sigma evk) ++
        strbrk " refers to a metavariable - please report your example" ++
        strbrk "at " ++ str Coq_config.wwwbugtracker ++ str "."]
     | InstanceNotSameType (evk,env,Some t,u) ->
        let t, u = pr_explicit env sigma t u in
        [str "unable to find a well-typed instantiation for " ++
        quote (pr_existential_key env sigma evk) ++
        strbrk ": cannot ensure that " ++
        t ++ strbrk " is a subtype of " ++ u]
     | InstanceNotSameType (evk,env,None,u) ->
        let u = pr_leconstr_env env sigma u in
        [str "unable to find a well-typed instantiation for " ++
        quote (pr_existential_key env sigma evk) ++
         strbrk " of type " ++ u]
     | InstanceNotFunctionalType (evk,env,f,u) ->
        let env = make_all_name_different env sigma in
        let f = pr_leconstr_env env sigma f in
        let u = pr_leconstr_env env sigma u in
        [str "unable to find a well-typed instantiation for " ++
        quote (pr_existential_key env sigma evk) ++
        strbrk ": " ++ f ++
        strbrk " is expected to have a functional type but it has type " ++ u]
     | UnifUnivInconsistency p ->
       [str "universe inconsistency: " ++
        UGraph.explain_universe_inconsistency
          (Termops.pr_evd_qvar sigma)
          (Termops.pr_evd_level sigma)
          p]
     | CannotSolveConstraint ((pb,env,t,u),e) ->
        let env = make_all_name_different env sigma in
        (strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++
        str " == " ++ pr_leconstr_env env sigma u)
        :: aux t u e
     | ProblemBeyondCapabilities ->
        []
     in
     match aux p1 p2 e with
     | [] -> mt ()
     | l -> spc () ++ str "(" ++
            prlist_with_sep pr_semicolon (fun x -> x) l ++ str ")"

let explain_actual_type env sigma j t reason =
  let env = make_all_name_different env sigma in
  let j = j_nf_betaiotaevar env sigma j in
  let t = Reductionops.nf_betaiota env sigma t in
  (* Actually print *)
  let pe = pr_ne_context_of (str "In environment") env sigma in
  let pc = pr_leconstr_env env sigma (Environ.j_val j) in
  let (pt, pct) = pr_explicit env sigma t (Environ.j_type j) in
  let ppreason = explain_unification_error env sigma j.uj_type t reason in
  pe ++
  hov 0 (
  str "The term" ++ brk(1,1) ++ pc ++ spc () ++
  str "has type" ++ brk(1,1) ++ pct ++ spc () ++
  str "while it is expected to have type" ++ brk(1,1) ++ pt ++
  ppreason ++ str ".")

let explain_incorrect_primitive env sigma j exp =
  let env = make_all_name_different env sigma in
  let {uj_val=p;uj_type=t} = j in
  let t = Reductionops.nf_betaiota env sigma t in
  let exp = Reductionops.nf_betaiota env sigma exp in
  (* Actually print *)
  let pe = pr_ne_context_of (str "In environment") env sigma in
  let (pt, pct) = pr_explicit env sigma exp t in
  pe ++
  hov 0 (
  str "The primitive" ++ brk(1,1) ++ str (CPrimitives.op_or_type_to_string p) ++ spc () ++
  str "has type" ++ brk(1,1) ++ pct ++ spc () ++
  str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str ".")

let explain_cant_apply_bad_type env sigma ?error (n,exptyp,actualtyp) rator randl =
  let randl = jv_nf_betaiotaevar env sigma randl in
  let actualtyp = Reductionops.nf_betaiota env sigma actualtyp in
  let env = make_all_name_different env sigma in
  let error = explain_unification_error env sigma actualtyp exptyp error in
  let actualtyp, exptyp = pr_explicit env sigma actualtyp exptyp in
  let nargs = Array.length randl in
(*  let pe = pr_ne_context_of (str "in environment") env sigma in*)
  let pr,prt = pr_ljudge_env env sigma rator in
  let term_string1 = str (String.plural nargs "term") in
  let term_string2 =
    if nargs>1 then str "The " ++ pr_nth n ++ str " term" else str "This term"
  in
  let appl = prvect_with_sep fnl
               (fun c ->
                  let pc,pct = pr_ljudge_env env sigma c in
                  hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl
  in
  str "Illegal application: " ++ (* pe ++ *) fnl () ++
  str "The term" ++ brk(1,1) ++ pr ++ spc () ++
  str "of type" ++ brk(1,1) ++ prt ++ spc () ++
  str "cannot be applied to the " ++ term_string1 ++ fnl () ++
  str " " ++ v 0 appl ++ fnl () ++ term_string2 ++ str " has type" ++
  brk(1,1) ++ actualtyp ++ spc () ++
  str "which should be a subtype of" ++ brk(1,1) ++
  exptyp ++ str "." ++ error

let explain_cant_apply_not_functional env sigma rator randl =
  let env = make_all_name_different env sigma in
  let nargs = Array.length randl in
(*  let pe = pr_ne_context_of (str "in environment") env sigma in*)
  let pr = pr_leconstr_env env sigma rator.uj_val in
  let prt = pr_leconstr_env env sigma rator.uj_type in
  let appl = prvect_with_sep fnl
               (fun c ->
                  let pc = pr_leconstr_env env sigma c.uj_val in
                  let pct = pr_leconstr_env env sigma c.uj_type in
                  hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl
  in
  str "Illegal application (Non-functional construction): " ++
  (* pe ++ *) fnl () ++
  str "The expression" ++ brk(1,1) ++ pr ++ spc () ++
  str "of type" ++ brk(1,1) ++ prt ++ spc () ++
  str "cannot be applied to the " ++ str (String.plural nargs "term") ++
  fnl () ++ str " " ++ v 0 appl

let explain_unexpected_type env sigma actual_type expected_type e =
  let pract, prexp = pr_explicit env sigma actual_type expected_type in
  str "Found type" ++ spc () ++ pract ++ spc () ++
  str "where" ++ spc () ++ prexp ++ str " was expected" ++
  explain_unification_error env sigma actual_type expected_type (Some e) ++ str"."

let explain_not_product env sigma c =
  let pr = pr_econstr_env env sigma c in
  str "The type of this term is a product" ++ spc () ++
  str "while it is expected to be" ++
  (if EConstr.isType sigma c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."

let explain_ill_formed_fix_body env sigma names i = function
  (* Fixpoint guard errors *)
  | NotEnoughAbstractionInFixBody ->
      str "Not enough abstractions in the definition"
  | RecursionNotOnInductiveType c ->
      str "Recursive definition on" ++ spc () ++ pr_leconstr_env env sigma c ++
      spc () ++ str "which should be a recursive inductive type"
  | RecursionOnIllegalTerm(j,(arg_env, arg),le_lt) ->
      let arg_env = make_all_name_different arg_env sigma in
      let called =
        match names.(j).binder_name with
            Name id -> Id.print id
          | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in
      let pr_db x = quote (pr_db env x) in
      let vars =
        match Lazy.force le_lt with
            ([],[]) -> assert false
          | ([x],[]) -> str "a subterm of " ++ pr_db x
          | (le,[]) -> str "a subterm of the following variables: " ++
              pr_sequence pr_db le
          | (_,[x]) -> pr_db x
          | (_,lt) ->
              str "one of the following variables: " ++
              pr_sequence pr_db lt in
      str "Recursive call to " ++ called ++ spc () ++
      strbrk "has principal argument equal to" ++ spc () ++
      pr_leconstr_env arg_env sigma arg ++ strbrk " instead of " ++ vars
  | NotEnoughArgumentsForFixCall j ->
      let called =
        match names.(j).binder_name with
            Name id -> Id.print id
          | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in
     str "Recursive call to " ++ called ++ str " has not enough arguments"
  | FixpointOnNonEliminable (s, s') ->
  let pr_sort u = quote @@ Flags.with_option Constrextern.print_universes (Printer.pr_sort sigma) u in
    fmt "Cannot define a fixpoint@ with principal argument living in sort %t@ \
         to produce a value in sort %t@ because %t does not eliminate to %t"
      (fun () -> pr_sort s)
      (fun () -> pr_sort s')
      (fun () -> pr_sort s)
      (fun () -> pr_sort s')

let explain_ill_formed_cofix_body env sigma = function
  (* CoFixpoint guard errors *)
  | CodomainNotInductiveType c ->
      str "The codomain is" ++ spc () ++ pr_leconstr_env env sigma c ++ spc () ++
      str "which should be a coinductive type"
  | NestedRecursiveOccurrences ->
      str "Nested recursive occurrences"
  | UnguardedRecursiveCall c ->
      str "Unguarded recursive call in" ++ spc () ++ pr_leconstr_env env sigma c
  | RecCallInTypeOfAbstraction c ->
      str "Recursive call forbidden in the domain of an abstraction:" ++
      spc () ++ pr_leconstr_env env sigma c
  | RecCallInNonRecArgOfConstructor c ->
      str "Recursive call on a non-recursive argument of constructor" ++
      spc () ++ pr_leconstr_env env sigma c
  | RecCallInTypeOfDef c ->
      str "Recursive call forbidden in the type of a recursive definition" ++
      spc () ++ pr_leconstr_env env sigma c
  | RecCallInCaseFun c ->
      str "Invalid recursive call in a branch of" ++
      spc () ++ pr_leconstr_env env sigma c
  | RecCallInCaseArg c ->
      str "Invalid recursive call in the argument of \"match\" in" ++ spc () ++
      pr_leconstr_env env sigma c
  | RecCallInCasePred c ->
      str "Invalid recursive call in the \"return\" clause of \"match\" in" ++
      spc () ++ pr_leconstr_env env sigma c
  | NotGuardedForm c ->
      str "Sub-expression " ++ pr_leconstr_env env sigma c ++
      strbrk " not in guarded form (should be a constructor," ++
      strbrk " an abstraction, a match, a cofix or a recursive call)"
  | ReturnPredicateNotCoInductive c ->
     str "The return clause of the following pattern matching should be" ++
     strbrk " a coinductive type:" ++
     spc () ++ pr_leconstr_env env sigma c

(* TODO: use the names *)
(* (co)fixpoints *)
let explain_ill_formed_rec_body env sigma err names i fixenv vdefj =
  let prt_name i =
    match names.(i).binder_name with
        Name id -> str "Recursive definition of " ++ Id.print id
      | Anonymous -> str "The " ++ pr_nth i ++ str " definition" in
  let st = match err with
    | FixGuardError err -> explain_ill_formed_fix_body env sigma names i err
    | CoFixGuardError  err -> explain_ill_formed_cofix_body env sigma err
  in
  prt_name i ++ str " is ill-formed." ++ fnl () ++
  pr_ne_context_of (str "In environment") env sigma ++
  st ++ str "." ++ fnl () ++
  (try (* May fail with unresolved globals. *)
      let fixenv = make_all_name_different fixenv sigma in
      let pvd = pr_leconstr_env fixenv sigma vdefj.(i).uj_val in
        str"Recursive definition is:" ++ spc () ++ pvd ++ str "."
    with e when CErrors.noncritical e -> mt ())

let explain_not_guarded env sigma cofix_err fix_errs (names, typs, defs as recdef) =
  let nfix = Array.length names in
  let lnames = Array.map_to_list binder_name names in
  let prt_names =
    hov 0 (str "Recursive definition of " ++ pr_enum Name.print lnames)
  in
  let st =
    (match cofix_err with
     | None -> mt ()
     | Some (env, i, err) ->
       (if nfix > 1 then str "As a mutual co-fixpoint:" else str "As a co-fixpoint:")
       ++ fnl() ++ explain_ill_formed_cofix_body env sigma err)
  in
  let stl =
    if List.exists (fun (env, i, nv, err) -> match err with RecursionOnIllegalTerm _ -> true | _ -> false) fix_errs then
      List.map (fun (env, i, nv, err) ->
          hov 0 ((if nfix > 1 then str "As a mutual fixpoint" else str "As a fixpoint")
                 ++ str " decreasing on the " ++ pr_enum (fun (n,na) -> pr_nth (n+1) ++ str " argument of " ++ Name.print na) (List.combine nv lnames) ++ str ":") ++
          fnl() ++ explain_ill_formed_fix_body env sigma names i err ++ str "." ++ fnl ())
        fix_errs
    else
      match fix_errs with
      | [] -> []
      | (env, i, nv, err) :: _ ->
        [hov 0 ((if nfix > 1 then str "As a mutual fixpoint" else str "As a fixpoint") ++ str ":") ++
          fnl() ++ explain_ill_formed_fix_body env sigma names i err ++ str "." ++ fnl ()]

      (* A common error independently on the decreasing argument *)
  in
  let fixenv = EConstr.push_rec_types recdef env in
  let st = prlist (fun x -> x) (st::stl) in
  prt_names ++ str " is ill-formed." ++ fnl () ++
  pr_ne_context_of (str "In environment") env sigma ++
  st ++
  prvecti_with_sep fnl (fun i v ->
      try (* May fail with unresolved globals. *)
        let fixenv = make_all_name_different fixenv sigma in
        let pvd = pr_leconstr_env fixenv sigma v in
        if nfix = 1 then
          str "Recursive definition is:" ++ spc () ++ pvd ++ str "."
        else
          str "The " ++ pr_nth (i+1) ++ str " recursive definition is:" ++ spc () ++ pvd ++ str "."
      with e when CErrors.noncritical e -> mt ())
    defs

let explain_ill_typed_rec_body env sigma i names vdefj vargs =
  let env = make_all_name_different env sigma in
  let pvd = pr_leconstr_env env sigma vdefj.(i).uj_val in
  let pvdt, pv = pr_explicit env sigma vdefj.(i).uj_type vargs.(i) in
  str "The " ++
  (match vdefj with [|_|] -> mt () | _ -> pr_nth (i+1) ++ spc ()) ++
  str "recursive definition" ++ spc () ++ pvd ++ spc () ++
  str "has type" ++ spc () ++ pvdt ++ spc () ++
  str "while it should be" ++ spc () ++ pv ++ str "."

let explain_cant_find_case_type env sigma c =
  let env = make_all_name_different env sigma in
  let pe = pr_leconstr_env env sigma c in
  str "Cannot infer the return type of pattern-matching on" ++ ws 1 ++
    pe ++ str "."

let explain_occur_check env sigma ev rhs =
  let env = make_all_name_different env sigma in
  let pt = pr_leconstr_env env sigma rhs in
  str "Cannot define " ++ pr_existential_key env sigma ev ++ str " with term" ++
  brk(1,1) ++ pt ++ spc () ++ str "that would depend on itself."

let pr_trailing_ne_context_of env sigma =
  if List.is_empty (Environ.rel_context env) &&
    List.is_empty (Environ.named_context env)
  then str "."
  else (strbrk " in environment:" ++ pr_context_unlimited env sigma)

let rec explain_evar_kind env sigma evk ty =
    let open Evar_kinds in
    function
  | Evar_kinds.NamedHole id ->
      strbrk "the existential variable named " ++ Id.print id
  | Evar_kinds.QuestionMark {qm_record_field=None} ->
      strbrk "this placeholder of type " ++ ty
  | Evar_kinds.QuestionMark {qm_record_field=Some {fieldname; recordname}} ->
          str "field " ++ (Printer.pr_constant env fieldname) ++ str " of record " ++ (Printer.pr_inductive env recordname)
  | Evar_kinds.CasesType false ->
      strbrk "the type of this pattern-matching problem"
  | Evar_kinds.CasesType true ->
      strbrk "a subterm of type " ++ ty ++
      strbrk " in the type of this pattern-matching problem"
  | Evar_kinds.BinderType (Name id) ->
      strbrk "the type of " ++ Id.print id
  | Evar_kinds.BinderType Anonymous ->
      strbrk "the type of this anonymous binder"
  | Evar_kinds.EvarType (ido,evk) ->
      let pp = match ido with
        | Some id -> str "?" ++ Id.print id
        | None ->
          try pr_existential_key env sigma evk
          with (* defined *) Not_found -> strbrk "an internal placeholder" in
      strbrk "the type of " ++ pp
  | Evar_kinds.ImplicitArg (c,(n,id),b) ->
      strbrk "the implicit parameter " ++ Id.print id ++ spc () ++ str "of" ++
      spc () ++ Nametab.pr_global_env Id.Set.empty c ++
      strbrk " whose type is " ++ ty
  | Evar_kinds.InternalHole -> strbrk "an internal placeholder of type " ++ ty
  | Evar_kinds.TomatchTypeParameter (tyi,n) ->
      strbrk "the " ++ pr_nth n ++
      strbrk " argument of the inductive type (" ++ pr_inductive env tyi ++
      strbrk ") of this term"
  | Evar_kinds.GoalEvar ->
      strbrk "an existential variable of type " ++ ty
  | Evar_kinds.ImpossibleCase ->
      strbrk "the type of an impossible pattern-matching clause"
  | Evar_kinds.MatchingVar _ ->
      assert false
  | Evar_kinds.VarInstance id ->
      strbrk "an instance of type " ++ ty ++
      str " for the variable " ++ Id.print id
  | Evar_kinds.SubEvar (where,evk') ->
      let rec find_source evk =
        let EvarInfo evi = Evd.find sigma evk in
        match snd (Evd.evar_source evi) with
        | Evar_kinds.SubEvar (_,evk) -> find_source evk
        | src -> EvarInfo evi, src in
      let EvarInfo evi, src = find_source evk' in
      let pc = match Evd.evar_body evi with
      | Evar_defined c -> pr_leconstr_env env sigma c
      | Evar_empty -> assert false in
      let ty' = match Evd.evar_body evi with
      | Evar_empty -> Evd.evar_concl evi
      | Evar_defined b -> Retyping.get_type_of env sigma b
      in
      pr_existential_key env sigma evk ++
      strbrk " in the partial instance " ++ pc ++
      strbrk " found for " ++
      explain_evar_kind env sigma evk
      (pr_leconstr_env env sigma ty') src

let explain_typeclass_resolution env sigma evi k =
  match Typeclasses.class_of_constr env sigma (Evd.evar_concl evi) with
  | Some _ ->
    let env = Evd.evar_filtered_env env evi in
      str "Could not find an instance for " ++
      pr_leconstr_env env sigma (Evd.evar_concl evi) ++
      pr_trailing_ne_context_of env sigma
  | _ -> mt()

let explain_placeholder_kind env sigma c e =
  match e with
  | Some (SeveralInstancesFound n) ->
      strbrk " (several distinct possible type class instances found)"
  | None ->
      match Typeclasses.class_of_constr env sigma c with
      | Some _ -> strbrk " (no type class instance found)"
      | _ -> mt ()

let explain_unsolvable_implicit env sigma evk explain =
  let evi = Evarutil.nf_evar_info sigma (Evd.find_undefined sigma evk) in
  let env = Evd.evar_filtered_env env evi in
  let type_of_hole = pr_leconstr_env env sigma (Evd.evar_concl evi) in
  let pe = pr_trailing_ne_context_of env sigma in
  strbrk "Cannot infer " ++
  explain_evar_kind env sigma evk type_of_hole (snd (Evd.evar_source evi)) ++
  explain_placeholder_kind env sigma (Evd.evar_concl evi) explain ++ pe

let explain_var_not_found env id =
  str "The variable" ++ spc () ++ Id.print id ++
  spc () ++ str "was not found" ++
  spc () ++ str "in the current" ++ spc () ++ str "environment" ++ str "."

let explain_evar_not_found env sigma id =
  let undef = Evar.Map.domain (Evd.undefined_map sigma) in
  let all_undef_evars = Evar.Set.elements undef in
  let f ev = Id.equal id (Termops.evar_suggested_name (Global.env ()) sigma ev) in
  if List.exists f all_undef_evars then
    (* The name is used for printing but is not user-given *)
    str "?" ++ Id.print id ++
    strbrk " is a generated name. Only user-given names for existential variables" ++
    strbrk " can be referenced. To give a user name to an existential variable," ++
    strbrk " introduce it with the ?[name] syntax."
  else
    str "Unknown existential variable."

let explain_wrong_case_info env (ind,u) ci =
  let pi = pr_inductive env ind in
  if QInd.equal env ci.ci_ind ind then
    str "Pattern-matching expression on an object of inductive type" ++
    spc () ++ pi ++ spc () ++ str "has invalid information."
  else
    let pc = pr_inductive env ci.ci_ind in
    str "A term of inductive type" ++ spc () ++ pi ++ spc () ++
    str "was given to a pattern-matching expression on the inductive type" ++
    spc () ++ pc ++ str "."

let explain_cannot_unify env sigma m n e =
  let env = make_all_name_different env sigma in
  let pm, pn = pr_explicit env sigma m n in
  let ppreason = explain_unification_error env sigma m n e in
  let pe = pr_ne_context_of (str "In environment") env sigma in
  pe ++ str "Unable to unify" ++ brk(1,1) ++ pm ++ spc () ++
  str "with" ++ brk(1,1) ++ pn ++ ppreason ++ str "."

let explain_cannot_unify_local env sigma m n subn =
  let pm = pr_leconstr_env env sigma m in
  let pn = pr_leconstr_env env sigma n in
  let psubn = pr_leconstr_env env sigma subn in
    str "Unable to unify" ++ brk(1,1) ++ pm ++ spc () ++
      str "with" ++ brk(1,1) ++ pn ++ spc () ++ str "as" ++ brk(1,1) ++
      psubn ++ str " contains local variables."

let explain_refiner_cannot_generalize env sigma ty =
  str "Cannot find a well-typed generalisation of the goal with type: " ++
  pr_leconstr_env env sigma ty ++ str "."

let explain_no_occurrence_found env sigma c id =
  str "Found no subterm matching" ++ spc() ++ pr_leconstr_env env sigma c ++
  spc() ++ str "in " ++
    (match id with
      | Some id -> Id.print id
      | None -> str"the current goal") ++ str "."

let explain_cannot_unify_binding_type env sigma m n =
  let pm = pr_leconstr_env env sigma m in
  let pn = pr_leconstr_env env sigma n in
  str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++
  str "which should be unifiable with" ++ brk(1,1) ++ pn ++ str "."

let explain_cannot_find_well_typed_abstraction env sigma p l e =
  str "Abstracting over the " ++
  str (String.plural (List.length l) "term") ++ spc () ++
  hov 0 (pr_enum (fun c -> pr_leconstr_env env sigma c) l) ++ spc () ++
  str "leads to a term" ++ spc () ++ pr_letype_env ~goal_concl_style:true env sigma p ++
  spc () ++ str "which is ill-typed." ++
  (match e with None -> mt () | Some e -> fnl () ++ str "Reason is: " ++ e)

let explain_wrong_abstraction_type env sigma na abs expected result =
  let ppname = match na with Name id -> Id.print id ++ spc () | _ -> mt () in
  str "Cannot instantiate metavariable " ++ ppname ++ strbrk "of type " ++
  pr_leconstr_env env sigma expected ++ strbrk " with abstraction " ++
  pr_leconstr_env env sigma abs ++ strbrk " of incompatible type " ++
  pr_leconstr_env env sigma result ++ str "."

let explain_abstraction_over_meta _ m n =
  strbrk "Too complex unification problem: cannot find a solution for both " ++
  Name.print m ++ spc () ++ str "and " ++ Name.print n ++ str "."

let explain_non_linear_unification env sigma m t =
  strbrk "Cannot unambiguously instantiate " ++
  Name.print m ++ str ":" ++
  strbrk " which would require to abstract twice on " ++
  pr_leconstr_env env sigma t ++ str "."

let explain_unsatisfied_constraints env sigma cst =
  let cst = Univ.Constraints.filter (fun cst -> not @@ UGraph.check_constraint (Evd.universes sigma) cst) cst in
  strbrk "Unsatisfied constraints: " ++
    Univ.Constraints.pr (Termops.pr_evd_level sigma) cst ++
    spc () ++ str "(maybe a bugged tactic)."

let explain_unsatisfied_qconstraints env sigma cst =
  strbrk "Unsatisfied quality constraints: " ++
  Sorts.QConstraints.pr (Termops.pr_evd_qvar sigma) cst ++
  spc() ++ str "(maybe a bugged tactic)."

let explain_undeclared_universes env sigma l =
  let l = Univ.Level.Set.elements l in
  strbrk "Undeclared " ++ str (CString.lplural l "universe") ++ strbrk ": " ++
  prlist_with_sep spc (Termops.pr_evd_level sigma) l ++
  spc () ++ str "(maybe a bugged tactic)."

let explain_undeclared_qualities env sigma l =
  let n = Sorts.QVar.Set.cardinal l in
  strbrk "Undeclared " ++ str (if n = 1 then "quality" else "qualities") ++ strbrk": " ++
    prlist_with_sep spc (Termops.pr_evd_qvar sigma) (Sorts.QVar.Set.elements l) ++
    spc () ++ str "(maybe a bugged tactic)."

let explain_disallowed_sprop () =
  Pp.(strbrk "SProp is disallowed because the "
      ++ str "\"Allow StrictProp\""
      ++ strbrk " flag is off.")

let pr_relevance sigma r =
  let r = EConstr.ERelevance.kind sigma r in
  match r with
  | Sorts.Relevant -> str "relevant"
  | Sorts.Irrelevant -> str "irrelevant"
  | Sorts.RelevanceVar q -> str "a variable " ++ (* TODO names *) Sorts.QVar.raw_pr q

let pr_binder env sigma = function
| LocalAssum (na, t) ->
  Pp.hov 2 (str "(" ++ (Name.print @@ na.binder_name) ++ str " : " ++
    pr_leconstr_env env sigma t ++ str ")")
| LocalDef (na, b, t) ->
  Pp.hov 2 (str "(" ++ (Name.print @@ na.binder_name) ++ str " : " ++
    pr_leconstr_env env sigma t ++ str " := " ++ pr_leconstr_env env sigma b ++ str ")")

let explain_bad_binder_relevance env sigma rlv decl =
  strbrk "Binder" ++ spc () ++ pr_binder env sigma decl ++
    strbrk " has relevance mark set to " ++ pr_relevance sigma (RelDecl.get_relevance decl) ++
    strbrk " but was expected to be " ++ pr_relevance sigma rlv ++
    spc () ++ str "(maybe a bugged tactic)."

let explain_bad_case_relevance env sigma rlv case =
  let (_, _, _, (_,badr), _, _, _) = EConstr.destCase sigma case in
  strbrk "Pattern-matching" ++ spc () ++ pr_leconstr_env env sigma case ++
    strbrk " has relevance mark set to " ++ pr_relevance sigma badr ++
    strbrk " but was expected to be " ++ pr_relevance sigma rlv ++
    spc () ++ str "(maybe a bugged tactic)."

let explain_bad_relevance env sigma = function
  | Typing.BadRelevanceCase (r,c) -> explain_bad_case_relevance env sigma r c
  | BadRelevanceBinder (r,d) -> explain_bad_binder_relevance env sigma r d

let () = CWarnings.register_printer Typing.bad_relevance_msg
    (fun (env, sigma, b) -> explain_bad_relevance env sigma b)

let explain_bad_invert env =
  strbrk "Bad case inversion (maybe a bugged tactic)."

let explain_bad_variance env sigma ~lev ~expected ~actual =
  fmt "Incorrect variance for universe %t:@ expected %t@ but cannot be less restrictive than %t."
    (fun () -> Termops.pr_evd_level sigma lev)
    (fun () -> UVars.Variance.pr expected)
    (fun () -> UVars.Variance.pr actual)

let explain_undeclared_used_variables env sigma ~declared_vars ~inferred_vars =
  let l = Id.Set.elements (Id.Set.diff inferred_vars declared_vars) in
  let n = List.length l in
  let declared_vars = Pp.pr_sequence Id.print (Id.Set.elements declared_vars) in
  let inferred_vars = Pp.pr_sequence Id.print (Id.Set.elements inferred_vars) in
  let missing_vars  = Pp.pr_sequence Id.print (List.rev l) in
  Pp.(prlist str
        ["The following section "; (String.plural n "variable"); " ";
         (String.conjugate_verb_to_be n); " used but not declared:"] ++ fnl () ++
      missing_vars ++ str "." ++ fnl () ++ fnl () ++
      str "You can either update your proof to not depend on " ++ missing_vars ++
      str ", or you can update your Proof line from" ++ fnl () ++
      str "Proof using " ++ declared_vars ++ fnl () ++
      str "to" ++ fnl () ++
      str "Proof using " ++ inferred_vars)

let explain_type_error env sigma err =
  let env = make_all_name_different env sigma in
  match err with
  | UnboundRel n ->
      explain_unbound_rel env sigma n
  | UnboundVar v ->
      explain_unbound_var env v
  | NotAType j ->
      explain_not_type env sigma j
  | BadAssumption c ->
      explain_bad_assumption env sigma c
  | ReferenceVariables (id,c) ->
      explain_reference_variables sigma id c
  | ElimArity (ind, c, okinds) ->
      explain_elim_arity env sigma ind (Some c) okinds
  | CaseNotInductive cj ->
      explain_case_not_inductive env sigma cj
  | CaseOnPrivateInd ind -> explain_case_on_private_ind env sigma ind
  | NumberBranches (cj, n) ->
      explain_number_branches env sigma cj n
  | IllFormedCaseParams -> explain_ill_formed_case_params env sigma
  | IllFormedBranch (c, i, actty, expty) ->
      explain_ill_formed_branch env sigma c i actty expty
  | Generalization (nvar, c) ->
      explain_generalization env sigma nvar c
  | ActualType (j, pt) ->
    explain_actual_type env sigma j pt None
  | IncorrectPrimitive (j, t) ->
    explain_incorrect_primitive env sigma j t
  | CantApplyBadType (t, rator, randl) ->
      explain_cant_apply_bad_type env sigma t rator randl
  | CantApplyNonFunctional (rator, randl) ->
      explain_cant_apply_not_functional env sigma rator randl
  | IllFormedRecBody (err, lna, i, fixenv, vdefj) ->
      explain_ill_formed_rec_body env sigma err lna i fixenv vdefj
  | IllTypedRecBody (i, lna, vdefj, vargs) ->
     explain_ill_typed_rec_body env sigma i lna vdefj vargs
  | WrongCaseInfo (ind,ci) ->
      explain_wrong_case_info env ind ci
  | UnsatisfiedConstraints cst ->
    explain_unsatisfied_constraints env sigma cst
  | UnsatisfiedQConstraints cst ->
    explain_unsatisfied_qconstraints env sigma cst
  | UndeclaredUniverses l ->
    explain_undeclared_universes env sigma l
  | UndeclaredQualities l ->
    explain_undeclared_qualities env sigma l
  | DisallowedSProp -> explain_disallowed_sprop ()
  | BadBinderRelevance (rlv, decl) -> explain_bad_binder_relevance env sigma rlv decl
  | BadCaseRelevance (rlv, case) -> explain_bad_case_relevance env sigma rlv case
  | BadInvert -> explain_bad_invert env
  | BadVariance {lev;expected;actual} -> explain_bad_variance env sigma ~lev ~expected ~actual
  | UndeclaredUsedVariables {declared_vars;inferred_vars} ->
      explain_undeclared_used_variables env sigma ~declared_vars ~inferred_vars

let pr_position (cl,pos) =
  let clpos = match cl with
    | None -> str " of the goal"
    | Some (id,Locus.InHyp) -> str " of hypothesis " ++ Id.print id
    | Some (id,Locus.InHypTypeOnly) -> str " of the type of hypothesis " ++ Id.print id
    | Some (id,Locus.InHypValueOnly) -> str " of the body of hypothesis " ++ Id.print id in
  int pos ++ clpos

let explain_cannot_unify_occurrences env sigma nested ((cl2,pos2),t2) ((cl1,pos1),t1) =
  if nested then
    str "Found nested occurrences of the pattern at positions " ++
    int pos1 ++ strbrk " and " ++ pr_position (cl2,pos2) ++ str "."
  else
    str "Found incompatible occurrences of the pattern" ++ str ":" ++
    spc () ++ str "Matched term " ++ pr_leconstr_env env sigma t2 ++
    strbrk " at position " ++ pr_position (cl2,pos2) ++
    strbrk " is not compatible with matched term " ++
    pr_leconstr_env env sigma t1 ++ strbrk " at position " ++
    pr_position (cl1,pos1) ++ str "."

let pr_constraints printenv msg env sigma evars cstrs =
  let (ev, evi) = Evar.Map.choose evars in
    if Evar.Map.for_all (fun ev' evi' ->
      eq_named_context_val (Evd.evar_hyps evi) (Evd.evar_hyps evi')) evars
    then
      let l = Evar.Map.bindings evars in
      let env' = Evd.evar_env env evi in
      let pe =
        if printenv then
          pr_ne_context_of (str "In environment:") env' sigma
        else mt ()
      in
      let env = Global.env () in
      let evs =
        prlist_with_sep (fun () -> fnl () ++ fnl ())
        (fun (ev, evi) -> hov 2 (pr_existential_key env sigma ev ++
            str " :" ++ spc () ++ Printer.pr_leconstr_env env' sigma (Evd.evar_concl evi))) l
      in
      h (pe ++ str msg ++ fnl () ++ evs ++ pr_evar_constraints sigma cstrs)
    else
      let filter evk _ = Evar.Map.mem evk evars in
      pr_evar_map_filter ~with_univs:false filter env sigma

let explain_unsatisfiable_constraints env sigma constr comp =
  let (_, constraints) = Evd.extract_all_conv_pbs sigma in
  let tcs = Evd.get_typeclass_evars sigma in
  let undef = Evd.undefined_map sigma in
  (* Only keep evars that are subject to resolution and members of the given
     component. *)
  let is_kept evk _ = Evar.Set.mem evk tcs && Evar.Set.mem evk comp in
  let undef =
    let m = Evar.Map.filter is_kept undef in
      if Evar.Map.is_empty m then undef
      else m
  in
  match constr with
  | None ->
    if List.is_empty constraints then
      let msg = "Could not find an instance for the following existential variables:" in
      pr_constraints true msg env sigma undef constraints
    else
      let msg = "Unable to satisfy the following constraints:" in
      pr_constraints true msg env sigma undef constraints
  | Some (ev, k) ->
    let cstr =
      let remaining = Evar.Map.remove ev undef in
      if not (Evar.Map.is_empty remaining) then
        let msg = "With the following constraints:" in
        pr_constraints false msg env sigma remaining constraints
      else mt ()
    in
    let info = Evar.Map.find ev undef in
    explain_typeclass_resolution env sigma info k ++ fnl () ++ cstr

let rec explain_pretype_error env sigma err =
  let env = Evardefine.env_nf_betaiotaevar sigma env in
  let env = make_all_name_different env sigma in
  match err with
  | CantFindCaseType c -> explain_cant_find_case_type env sigma c
  | ActualTypeNotCoercible (j,t,e) ->
    let {uj_val = c; uj_type = actty} = j in
    let (env, c, actty, expty), e = contract3' env sigma c actty t e in
    let j = {uj_val = c; uj_type = actty} in
    explain_actual_type env sigma j expty (Some e)
  | UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs
  | UnsolvableImplicit (evk,exp) -> explain_unsolvable_implicit env sigma evk exp
  | VarNotFound id -> explain_var_not_found env id
  | EvarNotFound id -> explain_evar_not_found env sigma id
  | UnexpectedType (actual,expect,e) ->
    let env, actual, expect = contract2 env sigma actual expect in
    explain_unexpected_type env sigma actual expect e
  | NotProduct c -> explain_not_product env sigma c
  | CannotUnify (m,n,e) ->
    let env, m, n = contract2 env sigma m n in
    explain_cannot_unify env sigma m n e
  | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn
  | CannotGeneralize ty -> explain_refiner_cannot_generalize env sigma ty
  | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env sigma c id
  | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env sigma m n
  | CannotFindWellTypedAbstraction (p,l,e) ->
      explain_cannot_find_well_typed_abstraction env sigma p l
        (Option.map (fun (env',e) -> explain_pretype_error env' sigma e) e)
  | WrongAbstractionType (n,a,t,u) ->
      explain_wrong_abstraction_type env sigma n a t u
  | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n
  | NonLinearUnification (m,c) -> explain_non_linear_unification env sigma m c
  | TypingError t -> explain_type_error env sigma t
  | CantApplyBadTypeExplained ((t, rator, randl),error) ->
    explain_cant_apply_bad_type env sigma ~error t rator randl
  | CannotUnifyOccurrences (b,c1,c2) -> explain_cannot_unify_occurrences env sigma b c1 c2
  | UnsatisfiableConstraints (c,comp) -> explain_unsatisfiable_constraints env sigma c comp
  | DisallowedSProp -> explain_disallowed_sprop ()

(* Module errors *)

let pr_modpath mp =
  Libnames.pr_qualid (Nametab.shortest_qualid_of_module mp)

let pr_modtype_subpath upper mp =
  let rec aux mp =
    try
      let (dir,id) = Libnames.repr_qualid (Nametab.shortest_qualid_of_modtype mp) in
      Libnames.add_dirpath_suffix dir id, []
    with Not_found ->
      match mp with
      | MPdot (mp',id) -> let mp, suff = aux mp' in mp, Label.to_id id::suff
      | _ -> assert false
  in
  let mp, suff = aux mp in
  (if suff = [] then mt ()
   else strbrk (if upper then "Module " else "module ") ++ DirPath.print (DirPath.make suff) ++ strbrk " of ") ++
  DirPath.print mp

let pr_module_or_modtype_subpath mp = match Nametab.shortest_qualid_of_module mp with
| qid ->
  (* [mp] is bound to a proper module *)
  strbrk "module " ++ Libnames.pr_qualid qid
| exception Not_found ->
  (* [mp] ought to be bound to a submodule of a module type *)
  pr_modtype_subpath false mp

open Modops

let explain_not_match_error = function
  | InductiveFieldExpected _ ->
    strbrk "an inductive definition is expected"
  | DefinitionFieldExpected ->
    strbrk "a definition is expected. Hint: you can rename the \
            inductive or constructor and add a definition mapping the \
            old name to the new name"
  | ModuleFieldExpected ->
    strbrk "a module is expected"
  | ModuleTypeFieldExpected ->
    strbrk "a module type is expected"
  | NotConvertibleInductiveField id | NotConvertibleConstructorField id ->
    str "types given to " ++ Id.print id ++ str " differ"
  | NotConvertibleBodyField ->
    str "the body of definitions differs"
  | NotConvertibleTypeField (env, typ1, typ2) ->
    let typ1, typ2 = pr_explicit env (Evd.from_env env) (EConstr.of_constr typ1) (EConstr.of_constr typ2) in
    str "expected type" ++ spc ()  ++
    typ2 ++ spc () ++
    str "but found type" ++ spc () ++
    typ1
  | NotSameConstructorNamesField ->
    str "constructor names differ"
  | NotSameInductiveNameInBlockField ->
    str "inductive types names differ"
  | FiniteInductiveFieldExpected isfinite ->
    str "type is expected to be " ++
    str (if isfinite then "coinductive" else "inductive")
  | InductiveNumbersFieldExpected n ->
    str "number of inductive types differs"
  | InductiveParamsNumberField n ->
    str "inductive type has not the right number of parameters"
  | RecordFieldExpected isrecord ->
    str "type is expected " ++ str (if isrecord then "" else "not ") ++
    str "to be a record"
  | RecordProjectionsExpected nal ->
    (if List.length nal >= 2 then str "expected projection names are "
     else str "expected projection name is ") ++
    pr_enum (function Name id -> Id.print id | _ -> str "_") nal
  | NotEqualInductiveAliases ->
    str "Aliases to inductive types do not match"
  | CumulativeStatusExpected b ->
    let status b = if b then str"cumulative" else str"non-cumulative" in
      str "a " ++ status b ++ str" declaration was expected, but a " ++
        status (not b) ++ str" declaration was found"
  | PolymorphicStatusExpected b ->
    let status b = if b then str"polymorphic" else str"monomorphic" in
      str "a " ++ status b ++ str" declaration was expected, but a " ++
        status (not b) ++ str" declaration was found"
  | IncompatibleUniverses incon ->
    str"the universe constraints are inconsistent: " ++
    UGraph.explain_universe_inconsistency
      Sorts.QVar.raw_pr
      UnivNames.pr_level_with_global_universes
      incon
  | IncompatiblePolymorphism (env, t1, t2) ->
    let t1, t2 = pr_explicit env (Evd.from_env env) (EConstr.of_constr t1) (EConstr.of_constr t2) in
    str "conversion of polymorphic values generates additional constraints: " ++
      quote t1 ++ spc () ++
      str "compared to " ++ spc () ++
      quote t2
  | IncompatibleConstraints { got; expect } ->
    let open UVars in
    let pr_auctx auctx =
      let sigma = Evd.from_ctx
          (UState.of_names
             (Printer.universe_binders_with_opt_names auctx None))
      in
      let uctx = AbstractContext.repr auctx in
      Printer.pr_universe_instance_binder sigma
        (UContext.instance uctx)
        (UContext.constraints uctx)
    in
    str "incompatible polymorphic binders: got" ++ spc () ++ h (pr_auctx got) ++ spc() ++
    str "but expected" ++ spc() ++ h (pr_auctx expect) ++
    (if not (UVars.eq_sizes (AbstractContext.size got) (AbstractContext.size expect)) then mt() else
       fnl() ++ str "(incompatible constraints)")
  | IncompatibleVariance ->
    str "incompatible variance information"
  | NoRewriteRulesSubtyping ->
    strbrk "subtyping for rewrite rule blocks is not supported"

let rec get_submodules acc = function
  | [] -> acc, []
  | Submodule l :: trace -> get_submodules (l::acc) trace
  | (FunctorArgument _ :: _) as trace -> acc, trace

let get_submodules trace =
  let submodules, trace = get_submodules [] trace in
  (String.concat "." (List.map Label.to_string submodules)), trace

let rec print_trace = function
  | [] -> assert false
  | (Submodule _ :: _) as trace ->
    let submodules, trace = get_submodules trace in
    str submodules ++
    (if List.is_empty trace then mt() else spc() ++ str "in " ++ print_trace trace)
  | FunctorArgument n :: trace ->
    str "the " ++ str (CString.ordinal n) ++ str " functor argument" ++
    (if List.is_empty trace then mt() else spc() ++ str "of " ++ print_trace trace)

let explain_signature_mismatch trace l why =
  let submodules, trace = get_submodules trace in
  let l = if String.is_empty submodules then Label.print l
    else str submodules ++ str"." ++ Label.print l
  in
  str "Signature components for field " ++ l ++
  (if List.is_empty trace then mt() else str " in " ++ print_trace trace) ++
  str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "."

let explain_label_already_declared l =
  str "The label " ++ Label.print l ++ str " is already declared."

let explain_not_a_functor () =
  str "Application of a non-functor."

let explain_is_a_functor mp =
  pr_modtype_subpath true mp ++ str " not expected to be a functor."

let explain_incompatible_module_types mexpr1 mexpr2 =
  let open Declarations in
  let open Mod_declarations in
  let rec get_arg = function
  | NoFunctor _ -> 0
  | MoreFunctor (_, _, ty) -> succ (get_arg ty)
  in
  let len1 = get_arg @@ mod_type mexpr1 in
  let len2 = get_arg @@ mod_type mexpr2 in
  if len1 <> len2 then
    str "Incompatible module types: module expects " ++ int len2 ++
      str " arguments, found " ++ int len1 ++ str "."
  else str "Incompatible module types."

let explain_not_equal_module_paths mp1 mp2 =
  str "Module " ++ pr_modpath mp1 ++ strbrk " is not equal to " ++ pr_module_or_modtype_subpath mp2 ++ str "."

let explain_no_such_label l mp =
  str "No field named " ++ Label.print l ++ str " in " ++ pr_modtype_subpath false mp ++ str "."

let explain_not_a_module_label l =
  Label.print l ++ str " is not the name of a module field."

let explain_not_a_constant l =
  quote (Label.print l) ++ str " is not a constant."

let explain_incorrect_label_constraint l =
  str "Incorrect constraint for label " ++
  quote (Label.print l) ++ str "."

let explain_generative_module_expected l =
  str "The module " ++ Label.print l ++ str " is not generative." ++
  strbrk " Only components of generative modules can be changed" ++
  strbrk " using the \"with\" construct."

let explain_label_missing l s =
  str "The field " ++ Label.print l ++ str " is missing in "
  ++ str s ++ str "."

let explain_include_restricted_functor mp =
  str "Cannot include the functor " ++ pr_modpath mp ++
  strbrk " since it has a restricted signature. " ++
  strbrk "You may name first an instance of this functor, and include it."

let explain_module_error = function
  | SignatureMismatch (trace,l,err) -> explain_signature_mismatch trace l err
  | LabelAlreadyDeclared l -> explain_label_already_declared l
  | NotAFunctor -> explain_not_a_functor ()
  | IsAFunctor mp -> explain_is_a_functor mp
  | IncompatibleModuleTypes (m1,m2) -> explain_incompatible_module_types m1 m2
  | NotEqualModulePaths (mp1,mp2) -> explain_not_equal_module_paths mp1 mp2
  | NoSuchLabel (l,mp) -> explain_no_such_label l mp
  | NotAModuleLabel l -> explain_not_a_module_label l
  | NotAConstant l -> explain_not_a_constant l
  | IncorrectWithConstraint l -> explain_incorrect_label_constraint l
  | GenerativeModuleExpected l -> explain_generative_module_expected l
  | LabelMissing (l,s) -> explain_label_missing l s
  | IncludeRestrictedFunctor mp -> explain_include_restricted_functor mp

(* Module internalization errors *)

(*
let explain_declaration_not_path _ =
  str "Declaration is not a path."

*)

let explain_not_module_nor_modtype qid =
  Libnames.pr_qualid qid ++ str " is not a module or module type."

let explain_not_a_module qid =
  Libnames.pr_qualid qid ++ str " is not a module."

let explain_not_a_module_type qid =
  Libnames.pr_qualid qid ++ str " is not a module type."

let explain_incorrect_with_in_module () =
  str "The syntax \"with\" is not allowed for modules."

let explain_incorrect_module_application () =
  str "Illegal application to a module type."

let explain_module_internalization_error = let open Modintern in function
  | NotAModuleNorModtype qid -> explain_not_module_nor_modtype qid
  | NotAModule qid -> explain_not_a_module qid
  | NotAModuleType qid -> explain_not_a_module_type qid
  | IncorrectWithInModule -> explain_incorrect_with_in_module ()
  | IncorrectModuleApplication -> explain_incorrect_module_application ()

(* Typeclass errors *)

let explain_not_a_class env sigma c =
  pr_econstr_env env sigma c ++ str" is not a declared type class."

let explain_unbound_method env sigma cid { CAst.v = id } =
  str "Unbound method name " ++ Id.print (id) ++ spc () ++
  str"of class" ++ spc () ++ pr_global cid ++ str "."

let explain_typeclass_error env sigma = function
  | NotAClass c -> explain_not_a_class env sigma c
  | UnboundMethod (cid, id) -> explain_unbound_method env sigma cid id

(* Refiner errors *)

let explain_refiner_unresolved_bindings l =
  str "Unable to find an instance for the " ++
  str (String.plural (List.length l) "variable") ++ spc () ++
  prlist_with_sep pr_comma Name.print l ++ str"."

let explain_refiner_cannot_apply env sigma t harg =
  str "In refiner, a term of type" ++ brk(1,1) ++
  pr_leconstr_env env sigma t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++
  pr_leconstr_env env sigma harg ++ str "."

let explain_intro_needs_product () =
  str "Introduction tactics needs products."

let explain_non_linear_proof env sigma c =
  str "Cannot refine with term" ++ brk(1,1) ++ pr_leconstr_env env sigma c ++
  spc () ++ str "because a metavariable has several occurrences."

let explain_no_such_hyp id =
  str "No such hypothesis: " ++ Id.print id

let explain_refiner_error env sigma = function
  | UnresolvedBindings t -> explain_refiner_unresolved_bindings t
  | CannotApply (t,harg) -> explain_refiner_cannot_apply env sigma t harg
  | IntroNeedsProduct -> explain_intro_needs_product ()
  | NonLinearProof c -> explain_non_linear_proof env sigma c
  | NoSuchHyp id -> explain_no_such_hyp id

(* Inductive errors *)

let error_non_strictly_positive env c v =
  let pc = pr_lconstr_env env (Evd.from_env env) c in
  let pv = pr_lconstr_env env (Evd.from_env env) v in
  str "Non strictly positive occurrence of " ++ pv ++ str " in" ++
  brk(1,1) ++ pc ++ str "."

let error_ill_formed_inductive env c v =
  let pc = pr_lconstr_env env (Evd.from_env env) c in
  let pv = pr_lconstr_env env (Evd.from_env env) v in
  str "Not enough arguments applied to the " ++ pv ++
  str " in" ++ brk(1,1) ++ pc ++ str "."

let error_ill_formed_constructor env id c v nparams nargs =
  let pv = pr_lconstr_env env (Evd.from_env env) v in
  let atomic = Int.equal (nb_prod Evd.empty (EConstr.of_constr c)) (* FIXME *) 0 in
  str "The type of constructor" ++ brk(1,1) ++ Id.print id ++ brk(1,1) ++
  str "is not valid;" ++ brk(1,1) ++
  strbrk (if atomic then "it must be " else "its conclusion must be ") ++
  pv ++
  (* warning: because of implicit arguments it is difficult to say which
     parameters must be explicitly given *)
  (if not (Int.equal nparams 0) then
    strbrk " applied to its " ++ str (String.plural nparams "parameter")
  else
    mt()) ++
  (if not (Int.equal nargs 0) then
     str (if not (Int.equal nparams 0) then " and" else " applied") ++
     strbrk " to some " ++ str (String.plural nargs "argument")
   else
     mt()) ++ str "."

let pr_ltype_using_barendregt_convention_env env c =
  (* Use goal_concl_style as an approximation of Barendregt's convention (?) *)
  quote (pr_ltype_env ~goal_concl_style:true env (Evd.from_env env) c)

let error_bad_ind_parameters env c n v1 v2  =
  let pc = pr_ltype_using_barendregt_convention_env env c in
  let pv1 = pr_lconstr_env env (Evd.from_env env) v1 in
  let pv2 = pr_lconstr_env env (Evd.from_env env) v2 in
  str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++
  str " as " ++ pr_nth n ++ str " argument in" ++ brk(1,1) ++ pc ++ str "."

let error_same_names_types id =
  str "The name" ++ spc () ++ Id.print id ++ spc () ++
  str "is used more than once."

let error_same_names_constructors id =
  str "The constructor name" ++ spc () ++ Id.print id ++ spc () ++
  str "is used more than once."

let error_same_names_overlap idl =
  strbrk "The following names are used both as type names and constructor " ++
  str "names:" ++ spc () ++
  prlist_with_sep pr_comma Id.print idl ++ str "."

let error_not_an_arity env c =
  str "The type" ++ spc () ++ pr_lconstr_env env (Evd.from_env env) c ++ spc () ++
  str "is not an arity."

let error_bad_entry () =
  str "Bad inductive definition."

let error_large_non_prop_inductive_not_in_type () =
  str "Large non-propositional inductive types must be in Type."

let error_inductive_missing_constraints env (us,ind_univ) =
  let sigma = Evd.from_env env in
  let pr_sort u = Flags.with_option Constrextern.print_universes (Printer.pr_sort sigma) u in
  str "Missing universe constraint declared for inductive type:" ++ spc()
  ++ v 0 (prlist_with_sep spc (fun u ->
      hov 0 (pr_sort u ++ str " <= " ++ pr_sort ind_univ))
      us)

(* Recursion schemes errors *)

let error_not_mutual_in_scheme env ind ind' =
  if QInd.equal env ind ind' then
    str "The inductive type " ++ pr_inductive env ind ++
    str " occurs twice."
  else
    str "The inductive types " ++ pr_inductive env ind ++ spc () ++
    str "and" ++ spc () ++ pr_inductive env ind' ++ spc () ++
    str "are not mutually defined."

(* Inductive constructions errors *)

let explain_inductive_error env = function
  | NonPos (c,v) -> error_non_strictly_positive env c v
  | NotEnoughArgs (c,v) -> error_ill_formed_inductive env c v
  | NotConstructor (id,c,v,n,m) ->
      error_ill_formed_constructor env id c v n m
  | NonPar (c,n,v1,v2) -> error_bad_ind_parameters env c n v1 v2
  | SameNamesTypes id -> error_same_names_types id
  | SameNamesConstructors id -> error_same_names_constructors id
  | SameNamesOverlap idl -> error_same_names_overlap idl
  | NotAnArity c -> error_not_an_arity env c
  | BadEntry -> error_bad_entry ()
  | LargeNonPropInductiveNotInType ->
    error_large_non_prop_inductive_not_in_type ()
  | MissingConstraints csts -> error_inductive_missing_constraints env csts

(* Primitive errors *)

let explain_incompatible_prim_declarations (type a) (act:a Primred.action_kind) (x:a) (y:a) =
  let open Primred in
  let env = Global.env() in
  (* The newer constant/inductive (either coming from Primitive or a
     Require) may be absent from the nametab as the error got raised
     while adding it to the safe_env. In that case we can't use
     nametab printing.

     There are still cases where the constant/inductive is added
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.46 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.