From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- ltac/taccoerce.ml | 344 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 344 insertions(+) create mode 100644 ltac/taccoerce.ml (limited to 'ltac/taccoerce.ml') diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml new file mode 100644 index 00000000..b0a80ef7 --- /dev/null +++ b/ltac/taccoerce.ml @@ -0,0 +1,344 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 normalize v = v + +let of_constr c = in_gen (topwit wit_constr) c + +let to_constr v = + let v = normalize v in + if has_type v (topwit wit_constr) then + let c = out_gen (topwit wit_constr) v in + Some c + else if has_type v (topwit wit_constr_under_binders) then + let vars, c = out_gen (topwit wit_constr_under_binders) v in + match vars with [] -> Some c | _ -> None + else None + +let of_uconstr c = in_gen (topwit wit_uconstr) c + +let to_uconstr v = + let v = normalize v in + if has_type v (topwit wit_uconstr) then + Some (out_gen (topwit wit_uconstr) v) + else None + +let of_int i = in_gen (topwit wit_int) i + +let to_int v = + let v = normalize v in + if has_type v (topwit wit_int) then + Some (out_gen (topwit wit_int) 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 + +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 = + Term.mkVar (let _ = Environ.lookup_named id env in id) + +(* Gives the constr corresponding to a Constr_context tactic_arg *) +let coerce_to_constr_context v = + let v = Value.normalize v in + if has_type v (topwit wit_constr_context) then + out_gen (topwit wit_constr_context) v + else raise (CannotCoerceTo "a term context") + +(* Interprets an identifier which must be fresh *) +let coerce_var_to_ident fresh env v = + let v = Value.normalize v in + let fail () = raise (CannotCoerceTo "a fresh identifier") in + if has_type v (topwit wit_intro_pattern) then + match out_gen (topwit wit_intro_pattern) v with + | _, IntroNaming (IntroIdentifier id) -> id + | _ -> fail () + else if has_type v (topwit wit_var) then + out_gen (topwit wit_var) 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 c && not (fresh && is_variable env (destVar c)) then + destVar 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 g env v = +let id_of_name = function + | Names.Anonymous -> Id.of_string "x" + | Names.Name x -> x in + let v = Value.normalize v in + let fail () = raise (CannotCoerceTo "an identifier") in + if has_type v (topwit wit_intro_pattern) then + match out_gen (topwit wit_intro_pattern) v with + | _, IntroNaming (IntroIdentifier id) -> id + | _ -> fail () + else if has_type v (topwit wit_var) then + out_gen (topwit wit_var) v + else + match Value.to_constr v with + | None -> fail () + | Some c -> + match Constr.kind c with + | Var id -> id + | Meta m -> id_of_name (Evd.meta_name g m) + | Evar (kn,_) -> + begin match Evd.evar_ident kn g with + | None -> fail () + | Some id -> id + end + | Const (cst,_) -> Label.to_id (Constant.label cst) + | Construct (cstr,_) -> + let ref = Globnames.ConstructRef cstr in + let basename = Nametab.basename_of_global ref in + basename + | Ind (ind,_) -> + let ref = Globnames.IndRef ind in + let basename = Nametab.basename_of_global ref in + basename + | Sort s -> + begin + match s with + | Prop _ -> Label.to_id (Label.make "Prop") + | Type _ -> Label.to_id (Label.make "Type") + end + | _ -> fail() + + +let coerce_to_intro_pattern env v = + let v = Value.normalize v in + if has_type v (topwit wit_intro_pattern) then + snd (out_gen (topwit wit_intro_pattern) v) + else if has_type v (topwit wit_var) then + let id = out_gen (topwit wit_var) v in + IntroNaming (IntroIdentifier id) + else match Value.to_constr v with + | Some c when isVar 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 c)) + | _ -> raise (CannotCoerceTo "an introduction pattern") + +let coerce_to_intro_pattern_naming env v = + match coerce_to_intro_pattern env v with + | IntroNaming pat -> pat + | _ -> raise (CannotCoerceTo "a naming introduction pattern") + +let coerce_to_hint_base v = + let v = Value.normalize v in + if has_type v (topwit wit_intro_pattern) then + match out_gen (topwit wit_intro_pattern) v with + | _, IntroNaming (IntroIdentifier id) -> Id.to_string id + | _ -> raise (CannotCoerceTo "a hint base name") + else raise (CannotCoerceTo "a hint base name") + +let coerce_to_int v = + let v = Value.normalize v in + 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 v = Value.normalize v in + let fail () = raise (CannotCoerceTo "a term") in + if has_type v (topwit wit_intro_pattern) then + match out_gen (topwit wit_intro_pattern) v with + | _, IntroNaming (IntroIdentifier id) -> + (try ([], constr_of_id env id) with Not_found -> fail ()) + | _ -> fail () + else if has_type v (topwit wit_constr) then + let c = out_gen (topwit wit_constr) v in + ([], c) + else if has_type v (topwit wit_constr_under_binders) then + out_gen (topwit wit_constr_under_binders) v + else if has_type v (topwit wit_var) then + let id = out_gen (topwit wit_var) v in + (try [], constr_of_id env id with Not_found -> fail ()) + else fail () + +let coerce_to_uconstr env v = + let v = Value.normalize v in + 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 v = + let fail () = raise (CannotCoerceTo "an evaluable reference") in + let v = Value.normalize v in + let ev = + if has_type v (topwit wit_intro_pattern) then + match out_gen (topwit wit_intro_pattern) v with + | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id + | _ -> fail () + else if has_type v (topwit wit_var) then + let id = out_gen (topwit wit_var) 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 Globnames 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 + match Value.to_constr v with + | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c)) + | Some c when isVar c -> EvalVarRef (destVar 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 env v = + match Value.to_list v with + | None -> raise (CannotCoerceTo "an intro pattern list") + | Some l -> + let map v = (loc, coerce_to_intro_pattern env v) in + List.map map l + +let coerce_to_hyp env v = + let fail () = raise (CannotCoerceTo "a variable") in + let v = Value.normalize v in + if has_type v (topwit wit_intro_pattern) then + match out_gen (topwit wit_intro_pattern) v with + | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id + | _ -> fail () + else if has_type v (topwit wit_var) then + let id = out_gen (topwit wit_var) v in + if is_variable env id then id else fail () + else match Value.to_constr v with + | Some c when isVar c -> destVar c + | _ -> fail () + +let coerce_to_hyp_list env v = + let v = Value.to_list v in + match v with + | Some l -> + let map n = coerce_to_hyp env n in + List.map map l + | None -> raise (CannotCoerceTo "a variable list") + +(* Interprets a qualified name *) +let coerce_to_reference env v = + let v = Value.normalize v in + match Value.to_constr v with + | Some c -> + begin + try Globnames.global_of_constr c + with Not_found -> 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 v = + let v = Value.normalize v in + if has_type v (topwit wit_intro_pattern) then + let v = out_gen (topwit wit_intro_pattern) v in + match v with + | _, IntroNaming (IntroIdentifier id) -> NamedHyp id + | _ -> raise (CannotCoerceTo "a quantified hypothesis") + else if has_type v (topwit wit_var) then + let id = out_gen (topwit wit_var) v in + NamedHyp 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 c -> NamedHyp (destVar 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 env v = + let v = Value.normalize v in + if has_type v (topwit wit_int) then + AnonHyp (out_gen (topwit wit_int) v) + else + try coerce_to_quantified_hypothesis v + with CannotCoerceTo _ -> + raise (CannotCoerceTo "a declared or quantified hypothesis") + +let coerce_to_int_or_var_list v = + match Value.to_list v with + | None -> raise (CannotCoerceTo "an int list") + | Some l -> + let map n = ArgArg (coerce_to_int n) in + List.map map l -- cgit v1.2.3