proofs/tacmach.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
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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 Namegen
open Termops
open Environ
open Reductionops
open Evd
open Typing
open Tacred
open Logic
open Context.Named.Declaration

module NamedDecl = Context.Named.Declaration

let re_sig it  gc = { it = it; sigma = gc; }

(**************************************************************)
(* Operations for handling terms under a local typing context *)
(**************************************************************)

type tactic = Proofview.V82.tac

let sig_it   = Refiner.sig_it
let project  = Refiner.project
let pf_env   = Refiner.pf_env
let pf_hyps  = Refiner.pf_hyps

let test_conversion env sigma pb c1 c2 =
  Reductionops.check_conv ~pb env sigma c1 c2

let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls)
let pf_hyps_types gls  =
  let sign = Environ.named_context (pf_env gls) in
  List.map (function LocalAssum (id,x)
                   | LocalDef (id,_,x) -> id, EConstr.of_constr x)
           sign

let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id

let pf_last_hyp gl = List.hd (pf_hyps gl)

let pf_get_hyp gls id =
  let env, sigma = pf_env gls, project gls in
  try
    Context.Named.lookup id (pf_hyps gls)
  with Not_found ->
    raise (RefinerError (env, sigma, NoSuchHyp id))

let pf_get_hyp_typ gls id =
  id |> pf_get_hyp gls |> NamedDecl.get_type

let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
let pf_ids_set_of_hyps gls =
  Environ.ids_of_named_context_val (Environ.named_context_val (pf_env gls))

let pf_get_new_id id gls =
  next_ident_away id (pf_ids_set_of_hyps gls)

let pf_apply f gls = f (pf_env gls) (project gls)
let pf_eapply f gls x = on_sig gls (fun evm -> f (pf_env gls) evm x)
let pf_reduce = pf_apply
let pf_e_reduce = pf_apply

let pf_whd_all         = pf_reduce whd_all
let pf_hnf_constr                = pf_reduce hnf_constr
let pf_nf                        = pf_reduce simpl
let pf_nf_betaiota               = pf_reduce nf_betaiota
let pf_compute                   = pf_reduce compute
let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
let pf_unsafe_type_of            = pf_reduce unsafe_type_of
let pf_type_of                   = pf_reduce type_of
let pf_get_type_of               = pf_reduce Retyping.get_type_of

let pf_conv_x gl                = pf_reduce test_conversion gl Reduction.CONV
let pf_const_value              = pf_reduce (fun env _ c -> EConstr.of_constr (constant_value_in env c))

let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
let pf_hnf_type_of gls          = pf_get_type_of gls %> pf_whd_all gls

(* Pretty-printers *)

open Pp

let db_pr_goal sigma g =
  let env = Goal.V82.env sigma g in
  let penv = Termops.Internal.print_named_context env in
  let pc = Termops.Internal.print_constr_env env sigma (Goal.V82.concl sigma g) in
  str"  " ++ hv 0 (penv ++ fnl () ++
                   str "============================" ++ fnl ()  ++
                   str" "  ++ pc) ++ fnl ()

let pr_gls gls =
  hov 0 (pr_evar_map (Some 2) (pf_env gls) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))

(* Variants of [Tacmach] functions built with the new proof engine *)
module New = struct

  let project gl =
    Proofview.Goal.sigma gl

  let pf_apply f gl =
    f (Proofview.Goal.env gl) (project gl)

  let of_old f gl =
    f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; }

  let pf_env = Proofview.Goal.env
  let pf_concl = Proofview.Goal.concl

  let pf_unsafe_type_of gl t =
    pf_apply unsafe_type_of gl t

  let pf_type_of gl t =
    pf_apply type_of gl t

  let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2

  let pf_ids_of_hyps gl =
    (* We only get the identifiers in [hyps] *)
    let hyps = Proofview.Goal.hyps gl in
    ids_of_named_context hyps

  let pf_ids_set_of_hyps gl =
    (* We only get the identifiers in [hyps] *)
    let env = Proofview.Goal.env gl in
    Environ.ids_of_named_context_val (Environ.named_context_val env)

  let pf_get_new_id id gl =
    let ids = pf_ids_set_of_hyps gl in
    next_ident_away id ids

  let pf_get_hyp id gl =
    let hyps = Proofview.Goal.env gl in
    let sigma = project gl in
    let sign =
      try EConstr.lookup_named id hyps
      with Not_found -> raise (RefinerError (hyps, sigma, NoSuchHyp id))
    in
    sign

  let pf_get_hyp_typ id gl =
    pf_get_hyp id gl |> NamedDecl.get_type

  let pf_hyps_types gl =
    let env = Proofview.Goal.env gl in
    let sign = Environ.named_context env in
    List.map (function LocalAssum (id,x)
                     | LocalDef (id,_,x) -> id.Context.binder_name, EConstr.of_constr x)
             sign

  let pf_last_hyp gl =
    let hyps = Proofview.Goal.hyps gl in
    List.hd hyps

  let pf_nf_concl (gl : Proofview.Goal.t) =
    (* We normalize the conclusion just after *)
    let concl = Proofview.Goal.concl gl in
    let sigma = project gl in
    nf_evar sigma concl

  let pf_whd_all gl t = pf_apply whd_all gl t

  let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t

  let pf_reduce_to_quantified_ind gl t =
    pf_apply reduce_to_quantified_ind gl t

  let pf_hnf_constr gl t = pf_apply hnf_constr gl t
  let pf_hnf_type_of gl t =
    pf_whd_all gl (pf_get_type_of gl t)

  let pf_compute gl t = pf_apply compute gl t

  let pf_nf_evar gl t = nf_evar (project gl) t
end