aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tacmach.ml
blob: 97c5cda7701c0a4b9ad43fc34891edf5da53f53e (plain)
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
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Util
open Namegen
open Termops
open Environ
open Reductionops
open Evd
open Typing
open Redexpr
open Tacred
open Proof_type
open Logic
open Refiner
open Sigma.Notations
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 'a sigma   = 'a Evd.sigma;;
type tactic     = Proof_type.tactic;;

let unpackage = Refiner.unpackage
let repackage = Refiner.repackage
let apply_sig_tac = Refiner.apply_sig_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 =
  try
    Context.Named.lookup id (pf_hyps gls)
  with Not_found ->
    raise (RefinerError (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_get_new_id id gls =
  next_ident_away id (pf_ids_of_hyps gls)

let pf_get_new_ids ids gls =
  let avoid = pf_ids_of_hyps gls in
  List.fold_right
    (fun id acc -> (next_ident_away id (acc@avoid))::acc)
    ids []

let pf_global gls id = EConstr.of_constr (Constrintern.construct_reference (pf_hyps gls) id)

let pf_reduction_of_red_expr gls re c =
  let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
  let sigma = Sigma.Unsafe.of_evar_map (project gls) in
  let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma c in
  (Sigma.to_evar_map sigma, c)

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 (fun _ -> 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_conv_x_leq gl            = pf_reduce test_conversion gl Reduction.CUMUL
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

let pf_is_matching gl p c       = pf_apply Constr_matching.is_matching_conv gl p c
let pf_matches gl p c           = pf_apply Constr_matching.matches_conv gl p c

(********************************************)
(* Definition of the most primitive tactics *)
(********************************************)

let refiner = refiner

let internal_cut_no_check replace id t gl =
  let t = EConstr.Unsafe.to_constr t in
  refiner (Cut (true,replace,id,t)) gl

let internal_cut_rev_no_check replace id t gl =
  let t = EConstr.Unsafe.to_constr t in
  refiner (Cut (false,replace,id,t)) gl

let refine_no_check c gl =
  let c = EConstr.Unsafe.to_constr c in
  refiner (Refine c) gl

(* Versions with consistency checks *)

let internal_cut b d t = with_check (internal_cut_no_check b d t)
let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
let refine c           = with_check (refine_no_check c)

(* Pretty-printers *)

open Pp

let db_pr_goal sigma g =
  let env = Goal.V82.env sigma g in
  let penv = print_named_context env in
  let pc = 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) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))

let pr_glls glls =
  hov 0 (pr_evar_map (Some 2) (sig_sig glls) ++ fnl () ++
         prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls))

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

  let project gl =
    let sigma = Proofview.Goal.sigma gl in
    Sigma.to_evar_map sigma

  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_global id gl =
    (** We only check for the existence of an [id] in [hyps] *)
    let gl = Proofview.Goal.assume gl in
    let hyps = Proofview.Goal.hyps gl in
    EConstr.of_constr (Constrintern.construct_reference hyps id)

  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 gl = Proofview.Goal.assume gl in
    let hyps = Proofview.Goal.hyps gl in
    ids_of_named_context hyps

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

  let pf_get_hyp id gl =
    let hyps = Proofview.Goal.env gl in
    let sign =
      try EConstr.lookup_named id hyps
      with Not_found -> raise (RefinerError (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, 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 : ([ `LZ ], 'r) Proofview.Goal.t) =
    (** We normalize the conclusion just after *)
    let gl = Proofview.Goal.assume gl in
    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_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t

  let pf_whd_all gl t = pf_apply whd_all gl t
  let pf_compute gl t = pf_apply compute gl t

  let pf_nf_evar gl t = nf_evar (project gl) t

end