Source file taccoerce.ml

(************************************************************************)
(*         *      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 Util
open Names
open Constr
open EConstr
open Namegen
open Tactypes
open Genarg
open Stdarg
open Tacarg
open Geninterp
open Pp

exception CannotCoerceTo of string

let pr_argument_type arg =
  let Val.Dyn (tag, _) = arg in
  Val.pr tag

(** TODO: unify printing of generic Ltac values in case of coercion failure. *)

(* Displays a value *)
let pr_value env v =
  let ppty = spc() ++ str "of type" ++ spc () ++ pr_argument_type v in
  let pr_with_env pr =
    match env with
    | Some (env,sigma) -> pr env sigma ++ ppty
    | None -> str "a value" ++ ppty
  in
  let open Genprint in
  match generic_val_print v with
  | TopPrinterBasic pr -> pr () ++ ppty
  | TopPrinterNeedsContext pr -> pr_with_env pr
  | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
     pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)

(** Abstract application, to print ltac functions *)
type appl =
  | UnnamedAppl (** For generic applications: nothing is printed *)
  | GlbAppl of (Names.KerName.t * Val.t list) list
       (** For calls to global constants, some may alias other. *)

(* Values for interpretation *)
type tacvalue =
  | VFun of
      appl *
      Tacexpr.ltac_trace *
      Loc.t option * (* when executing a global Ltac function: the location where this function was called *)
      Val.t Id.Map.t * (* closure *)
      Name.t list * (* binders *)
      Tacexpr.glob_tactic_expr (* body *)
  | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr

let tacvalue_tag : tacvalue Val.typ =
  let tag = Val.create "tacvalue" in
  let pr = function
    | VFun (a,_,loc,ids,l,tac) ->
      let tac = if List.is_empty l then tac else CAst.make ?loc @@ Tacexpr.TacFun (l,tac) in
      let pr_env env sigma = if Id.Map.is_empty ids then mt () else cut () ++ str "where" ++ Id.Map.fold (fun id c pp -> cut () ++ Id.print id ++ str " := " ++ pr_value (Some (env,sigma)) c ++ pp) ids (mt ()) in
      Genprint.TopPrinterNeedsContext (fun env sigma -> v 0 (hov 0 (Pptactic.pr_glob_tactic env tac) ++ pr_env env sigma))
    | _ -> Genprint.TopPrinterBasic (fun _ -> str "<tactic closure>") in
  let () = Genprint.register_val_print0 tag pr in
  tag

let constr_context_tag : Constr_matching.context Val.typ =
  let tag = Val.create "constr_context" in
  let pr env sigma lev c : Pp.t = Printer.pr_econstr_n_env env sigma lev (Constr_matching.repr_context c) in
  let () = Genprint.register_val_print0 tag (Pptactic.make_constr_printer pr) in
  tag

(* includes idents known to be bound and references *)
let constr_under_binders_tag : Ltac_pretype.constr_under_binders Val.typ =
  let tag = Val.create "constr_under_binders" in
  let () = Genprint.register_val_print0 tag (fun c ->
      Genprint.TopPrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in
  tag

(** All the types considered here are base types *)
let val_tag wit = match val_tag wit with
| Val.Base t -> t
| _ -> assert false

let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
  let Val.Dyn (t, _) = v in
  match Val.eq t (val_tag wit) with
  | None -> false
  | Some Refl -> true

let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
  let Val.Dyn (t', x) = v in
  match Val.eq t t' with
  | None -> None
  | Some Refl -> Some x

let in_gen wit v = Val.Dyn (val_tag wit, v)
let out_gen wit v = match prj (val_tag wit) v with None -> assert false | Some x -> x

module Value =
struct

type t = Val.t

let of_tacvalue v = Val.Dyn (tacvalue_tag, v)

let to_tacvalue v = prj tacvalue_tag v

let of_constr c = in_gen (topwit wit_constr) c

let to_constr v =
  if has_type v (topwit wit_constr) then
    let c = out_gen (topwit wit_constr) v in
    Some c
  else match prj constr_under_binders_tag v with
    | Some (vars, c) ->
      begin match vars with [] -> Some c | _ -> None end
    | None ->  None

let of_uconstr c = in_gen (topwit wit_uconstr) c

let to_uconstr v =
  if has_type v (topwit wit_uconstr) then
    Some (out_gen (topwit wit_uconstr) v)
  else None

let of_constr_context v = Val.Dyn (constr_context_tag, v)

let to_constr_context v = prj constr_context_tag v

(* XXX should we do [of_constr] when the vars are empty? *)
let of_constr_under_binders v = Val.Dyn (constr_under_binders_tag, v)

let of_int i = in_gen (topwit wit_int) i

let to_int v =
  if has_type v (topwit wit_int) then
    Some (out_gen (topwit wit_int) v)
  else None

let of_ident id = in_gen (topwit wit_ident) id

let to_ident v =
  if has_type v (topwit wit_ident) then
    Some (out_gen (topwit wit_ident) v)
  else None

let to_list v = prj Val.typ_list v

let to_option v = prj Val.typ_opt v

let to_pair v = prj Val.typ_pair v

let cast_error wit v =
  let pr_v = Pptactic.pr_value Pptactic.ltop v in
  let Val.Dyn (tag, _) = v in
  let tag = Val.pr tag in
  CErrors.user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
    ++ str " while type " ++ Val.pr wit ++ str " was expected.")

let unbox wit v ans = match ans with
| None -> cast_error wit v
| Some x -> x

let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with
| Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v))
| Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v))
| Val.Pair (tag1, tag2) ->
  let (x, y) = unbox Val.typ_pair v (to_pair v) in
  (prj tag1 x, prj tag2 y)
| Val.Base t ->
  let Val.Dyn (t', x) = v in
  match Val.eq t t' with
  | None -> cast_error t v
  | Some Refl -> x
let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with
| ExtraArg _ -> Geninterp.val_tag (topwit wit)
| ListArg t -> Val.List (tag_of_arg t)
| OptArg t -> Val.Opt (tag_of_arg t)
| PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2)

let val_cast arg v = prj (tag_of_arg arg) v

let cast (Topwit wit) v = val_cast wit v

end

let is_variable env id =
  Id.List.mem id (Termops.ids_of_named_context (Environ.named_context env))

(* Transforms an id into a constr if possible, or fails with Not_found *)
let constr_of_id env id =
  EConstr.mkVar (let _ = Environ.lookup_named id env in id)

(* Gives the Value.t corresponding to a Constr_context tactic_arg *)
let coerce_to_constr_context v =
  match Value.to_constr_context v with
  | Some v -> v
  | None -> raise (CannotCoerceTo "a term context")

let is_intro_pattern v =
  if has_type v (topwit wit_intro_pattern) then
    Some (out_gen (topwit wit_intro_pattern) v).CAst.v
  else
    None

(* Interprets an identifier which must be fresh *)
let coerce_var_to_ident fresh env sigma v =
  let fail () = raise (CannotCoerceTo "a fresh identifier") in
  match is_intro_pattern v with
  | Some (IntroNaming (IntroIdentifier id)) -> id
  | Some _ -> fail ()
  | None ->
  if has_type v (topwit wit_intro_pattern) then
    match out_gen (topwit wit_intro_pattern) v with
    | { CAst.v=IntroNaming (IntroIdentifier id)} -> id
    | _ -> fail ()
  else if has_type v (topwit wit_hyp) then
    out_gen (topwit wit_hyp) v
  else match Value.to_constr v with
  | None -> fail ()
  | Some c ->
    (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *)
    if isVar sigma c && not (fresh && is_variable env (destVar sigma c)) then
      destVar sigma c
    else fail ()


(* Interprets, if possible, a constr to an identifier which may not
   be fresh but suitable to be given to the fresh tactic. Works for
   vars, constants, inductive, constructors and sorts. *)
let coerce_to_ident_not_fresh sigma v =
  let fail () = raise (CannotCoerceTo "an identifier") in
  match is_intro_pattern v with
  | Some (IntroNaming (IntroIdentifier id)) -> id
  | Some _ -> fail ()
  | None ->
  if has_type v (topwit wit_hyp) then
    out_gen (topwit wit_hyp) v
  else
    match Value.to_constr v with
    | None -> fail ()
    | Some c ->
       match EConstr.kind sigma c with
       | Var id -> id
       | Meta m -> Id.of_string "x"
       | Evar (kn,_) ->
        begin match Evd.evar_ident kn sigma with
        | None -> fail ()
        | Some id -> id
        end
       | Const (cst,_) -> Label.to_id (Constant.label cst)
       | Construct (cstr,_) ->
          let ref = GlobRef.ConstructRef cstr in
          let basename = Nametab.basename_of_global ref in
          basename
       | Ind (ind,_) ->
          let ref = GlobRef.IndRef ind in
          let basename = Nametab.basename_of_global ref in
          basename
       | Sort s ->
          begin
            match ESorts.kind sigma s with
            | Sorts.SProp -> Label.to_id (Label.make "SProp")
            | Sorts.Prop -> Label.to_id (Label.make "Prop")
            | Sorts.Set -> Label.to_id (Label.make "Set")
            | Sorts.Type _ | Sorts.QSort _ -> Label.to_id (Label.make "Type")
          end
       | _ -> fail()


let coerce_to_intro_pattern sigma v =
  match is_intro_pattern v with
  | Some pat -> pat
  | None ->
  if has_type v (topwit wit_hyp) then
    let id = out_gen (topwit wit_hyp) v in
    IntroNaming (IntroIdentifier id)
  else match Value.to_constr v with
  | Some c when isVar sigma c ->
      (* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
      (* but also in "destruct H as (H,H')" *)
      IntroNaming (IntroIdentifier (destVar sigma c))
  | _ -> raise (CannotCoerceTo "an introduction pattern")

let coerce_to_intro_pattern_naming sigma v =
  match coerce_to_intro_pattern sigma v with
  | IntroNaming pat -> pat
  | _ -> raise (CannotCoerceTo "a naming introduction pattern")

let coerce_to_hint_base v =
  match is_intro_pattern v with
  | Some (IntroNaming (IntroIdentifier id)) -> Id.to_string id
  | Some _ | None -> raise (CannotCoerceTo "a hint base name")

let coerce_to_int v =
  if has_type v (topwit wit_int) then
    out_gen (topwit wit_int) v
  else raise (CannotCoerceTo "an integer")

let coerce_to_constr env v =
  let fail () = raise (CannotCoerceTo "a term") in
  match is_intro_pattern v with
  | Some (IntroNaming (IntroIdentifier id)) ->
      (try ([], constr_of_id env id) with Not_found -> fail ())
  | Some _ -> fail ()
  | None ->
  if has_type v (topwit wit_constr) then
    let c = out_gen (topwit wit_constr) v in
    ([], c)
  else match prj constr_under_binders_tag v with
  | Some v -> v
  | None ->
  if has_type v (topwit wit_hyp) then
    let id = out_gen (topwit wit_hyp) v in
    (try [], constr_of_id env id with Not_found -> fail ())
  else fail ()

let coerce_to_uconstr v =
  if has_type v (topwit wit_uconstr) then
    out_gen (topwit wit_uconstr) v
  else
    raise (CannotCoerceTo "an untyped term")

let coerce_to_closed_constr env v =
  let ids,c = coerce_to_constr env v in
  let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in
  c

let coerce_to_evaluable_ref env sigma v =
  let open Evaluable in
  let fail () = raise (CannotCoerceTo "an evaluable reference") in
  let ev =
  match is_intro_pattern v with
  | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> EvalVarRef id
  | Some _ -> fail ()
  | None ->
  if has_type v (topwit wit_hyp) then
    let id = out_gen (topwit wit_hyp) v in
    if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
    else fail ()
  else if has_type v (topwit wit_ref) then
    let open GlobRef in
    let r = out_gen (topwit wit_ref) v in
    match r with
    | VarRef var -> EvalVarRef var
    | ConstRef c -> EvalConstRef c
    | IndRef _ | ConstructRef _ -> fail ()
  else if has_type v (topwit wit_smart_global) then
    let open GlobRef in
    let r = out_gen (topwit wit_smart_global) v in
    match r with
    | VarRef var -> EvalVarRef var
    | ConstRef c -> EvalConstRef c
    | IndRef _ | ConstructRef _ -> fail ()
  else
    match Value.to_constr v with
    | Some c when isConst sigma c -> EvalConstRef (fst (destConst sigma c))
    | Some c when isVar sigma c -> EvalVarRef (destVar sigma c)
    | _ -> fail ()
  in if Tacred.is_evaluable env ev then ev else fail ()

let coerce_to_constr_list env v =
  let v = Value.to_list v in
  match v with
  | Some l ->
    let map v = coerce_to_closed_constr env v in
    List.map map l
  | None -> raise (CannotCoerceTo "a term list")

let coerce_to_intro_pattern_list ?loc sigma v =
  match Value.to_list v with
  | None -> raise (CannotCoerceTo "an intro pattern list")
  | Some l ->
    let map v = CAst.make ?loc @@ coerce_to_intro_pattern sigma v in
    List.map map l

let coerce_to_hyp env sigma v =
  let fail () = raise (CannotCoerceTo "a variable") in
  match is_intro_pattern v with
  | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> id
  | Some _ -> fail ()
  | None ->
  if has_type v (topwit wit_hyp) then
    let id = out_gen (topwit wit_hyp) v in
    if is_variable env id then id else fail ()
  else match Value.to_constr v with
  | Some c when isVar sigma c -> destVar sigma c
  | _ -> fail ()

let coerce_to_hyp_list env sigma v =
  let v = Value.to_list v in
  match v with
  | Some l ->
    let map n = coerce_to_hyp env sigma n in
    List.map map l
  | None -> raise (CannotCoerceTo "a variable list")

(* Interprets a qualified name *)
let coerce_to_reference sigma v =
  match Value.to_constr v with
  | Some c ->
    begin
      try fst (EConstr.destRef sigma c)
      with DestKO -> raise (CannotCoerceTo "a reference")
    end
  | None -> raise (CannotCoerceTo "a reference")

(* Quantified named or numbered hypothesis or hypothesis in context *)
(* (as in Inversion) *)
let coerce_to_quantified_hypothesis sigma v =
  match is_intro_pattern v with
  | Some (IntroNaming (IntroIdentifier id)) -> NamedHyp (CAst.make id)
  | Some _ -> raise (CannotCoerceTo "a quantified hypothesis")
  | None ->
  if has_type v (topwit wit_hyp) then
    let id = out_gen (topwit wit_hyp) v in
    NamedHyp (CAst.make id)
  else if has_type v (topwit wit_int) then
    AnonHyp (out_gen (topwit wit_int) v)
  else match Value.to_constr v with
  | Some c when isVar sigma c -> NamedHyp (CAst.make @@ destVar sigma c)
  | _ -> raise (CannotCoerceTo "a quantified hypothesis")

(* Quantified named or numbered hypothesis or hypothesis in context *)
(* (as in Inversion) *)
let coerce_to_decl_or_quant_hyp sigma v =
  if has_type v (topwit wit_int) then
    AnonHyp (out_gen (topwit wit_int) v)
  else
    try coerce_to_quantified_hypothesis sigma v
    with CannotCoerceTo _ ->
      raise (CannotCoerceTo "a declared or quantified hypothesis")

let coerce_to_int_list v =
  match Value.to_list v with
  | None -> raise (CannotCoerceTo "an int list")
  | Some l ->
    List.map coerce_to_int l

exception CoercionError of Id.t * (Environ.env * Evd.evar_map) option * Val.t * string

let () = CErrors.register_handler begin function
| CoercionError (id, env, v, s) ->
  Some (str "Ltac variable " ++ Id.print id ++
   strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
   strbrk "which cannot be coerced to " ++ str s ++ str".")
| _ -> None
end

let error_ltac_variable ?loc id env v s =
  Loc.raise ?loc (CoercionError (id, env, v, s))