package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file evar_tactics.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq 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 Context
open CErrors
open Evar_refiner
open Tacexpr
open Locus
open Context.Named.Declaration
open Ltac_pretype

module NamedDecl = Context.Named.Declaration

(* The instantiate tactic *)

let instantiate_evar evk (ist,rawc) =
  let open Proofview.Notations in
  Proofview.tclENV >>= fun env ->
  Proofview.Goal.enter begin fun gl ->
  let sigma = Proofview.Goal.sigma gl in
  let evi = Evd.find sigma evk in
  let filtered = Evd.evar_filtered_env env evi in
  let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
  let lvar = {
    ltac_constrs = constrvars;
    ltac_uconstrs = Names.Id.Map.empty;
    ltac_idents = Names.Id.Map.empty;
    ltac_genargs = ist.Geninterp.lfun;
  } in
  let sigma' = w_refine (evk,evi) (lvar ,rawc) env sigma in
  Proofview.Unsafe.tclEVARS sigma'
  end

let evar_list sigma c =
  let rec evrec acc c =
    match EConstr.kind sigma c with
    | Evar (evk, _ as ev) -> ev :: acc
    | _ -> EConstr.fold sigma evrec acc c in
  evrec [] c

let instantiate_tac n c ido =
  Proofview.Goal.enter begin fun gl ->
  let sigma = Proofview.Goal.sigma gl in
  let env = Proofview.Goal.env gl in
  let concl = Proofview.Goal.concl gl in
  let evl =
    match ido with
        ConclLocation () -> evar_list sigma concl
      | HypLocation (id,hloc) ->
          let decl = Environ.lookup_named id env in
            match hloc with
                InHyp ->
                  (match decl with
                    | LocalAssum (_,typ) -> evar_list sigma (EConstr.of_constr typ)
                    | _ -> user_err Pp.(str "Please be more specific: in type or value?"))
              | InHypTypeOnly ->
                  evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl))
              | InHypValueOnly ->
                  (match decl with
                    | LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body)
                    | _ -> user_err Pp.(str "Not a defined hypothesis.")) in
  if List.length evl < n then
    user_err Pp.(str "Not enough uninstantiated existential variables.");
  if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
  let evk,_ = List.nth evl (n-1) in
  instantiate_evar evk c
  end

let instantiate_tac_by_name id c =
  Proofview.Goal.enter begin fun gl ->
  let sigma = Proofview.Goal.sigma gl in
  let evk =
    try Evd.evar_key id sigma
    with Not_found -> user_err Pp.(str "Unknown existential variable.") in
  instantiate_evar evk c
  end

let let_evar name typ =
  let src = (Loc.tag Evar_kinds.GoalEvar) in
  Proofview.Goal.enter begin fun gl ->
    let sigma = Tacmach.New.project gl in
    let env = Proofview.Goal.env gl in
    let sigma, _ = Typing.sort_of env sigma typ in
    let id = match name with
    | Name.Anonymous ->
      let id = Namegen.id_of_name_using_hdchar env sigma typ name in
      Namegen.next_ident_away_in_goal id (Termops.vars_of_env env)
    | Name.Name id -> id
    in
    let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Namegen.IntroFresh id) typ in
    Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
    (Tactics.pose_tac (Name.Name id) evar)
  end

let hget_evar n =
  let open EConstr in
  Proofview.Goal.enter begin fun gl ->
  let sigma = Tacmach.New.project gl in
  let concl = Proofview.Goal.concl gl in
  let evl = evar_list sigma concl in
  if List.length evl < n then
    user_err Pp.(str "Not enough uninstantiated existential variables.");
  if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
  let ev = List.nth evl (n-1) in
  let ev_type = EConstr.existential_type sigma ev in
  let r = Retyping.relevance_of_type (Proofview.Goal.env gl) sigma ev_type in
  Tactics.change_concl (mkLetIn (make_annot Name.Anonymous r,mkEvar ev,ev_type,concl))
  end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct