Quelle taccoerce.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 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 "") 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))

quality99%

¤ Dauer der Verarbeitung: 0.10 Sekunden ¤

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.