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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Util
open Pp
module NamedDecl = Context.Named.Declaration
(* This module implements the abstract interface to goals *)
(* A general invariant of the module, is that a goal whose associated
evar is defined in the current evar_map, should not be accessed. *)
(* type of the goals *)
type goal = Evd.evar
let pr_goal e = str "GOAL:" ++ Pp.int (Evar.repr e)
let uid e = string_of_int (Evar.repr e)
(* Layer to implement v8.2 tactic engine ontop of the new architecture.
Types are different from what they used to be due to a change of the
internal types. *)
module V82 = struct
(* Old style env primitive *)
let env evars gl =
let evi = Evd.find evars gl in
Evd.evar_filtered_env evi
(* Old style hyps primitive *)
let hyps evars gl =
let evi = Evd.find evars gl in
Evd.evar_filtered_hyps evi
(* same as [hyps], but ensures that existential variables are
normalised. *)
let nf_hyps evars gl =
let hyps = Environ.named_context_of_val (hyps evars gl) in
Environ.val_of_named_context (Evarutil.nf_named_context_evar evars hyps)
(* Access to ".evar_concl" *)
let concl evars gl =
let evi = Evd.find evars gl in
EConstr.of_constr evi.Evd.evar_concl
(* Access to ".evar_extra" *)
let extra evars gl =
let evi = Evd.find evars gl in
evi.Evd.evar_extra
(* Old style mk_goal primitive *)
let mk_goal evars hyps concl extra =
(* A goal created that way will not be used by refine and will not
be shelved. It must not appear as a future_goal, so the future
goals are restored to their initial value after the evar is
created. *)
let concl = EConstr.Unsafe.to_constr concl in
let prev_future_goals = Evd.future_goals evars in
let prev_principal_goal = Evd.principal_future_goal evars in
let evi = { Evd.evar_hyps = hyps;
Evd.evar_concl = concl;
Evd.evar_filter = Evd.Filter.identity;
Evd.evar_body = Evd.Evar_empty;
Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
Evd.evar_candidates = None;
Evd.evar_extra = extra }
in
let evi = Typeclasses.mark_unresolvable evi in
let (evars, evk) = Evarutil.new_pure_evar_full evars evi in
let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in
let ctxt = Environ.named_context_of_val hyps in
let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
let ev = EConstr.mkEvar (evk,inst) in
(evk, ev, evars)
(* Instantiates a goal with an open term *)
let partial_solution sigma evk c =
(* Check that the goal itself does not appear in the refined term *)
let _ =
if not (Evarutil.occur_evar_upto sigma evk c) then ()
else Pretype_errors.error_occur_check Environ.empty_env sigma evk c
in
Evd.define evk (EConstr.Unsafe.to_constr c) sigma
(* Instantiates a goal with an open term, using name of goal for evk' *)
let partial_solution_to sigma evk evk' c =
let id = Evd.evar_ident evk sigma in
let sigma = partial_solution sigma evk c in
match id with
| None -> sigma
| Some id -> Evd.rename evk' id sigma
(* Parts of the progress tactical *)
let same_goal evars1 gl1 evars2 gl2 =
let evi1 = Evd.find evars1 gl1 in
let evi2 = Evd.find evars2 gl2 in
Term.eq_constr evi1.Evd.evar_concl evi2.Evd.evar_concl &&
Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps
let weak_progress glss gls =
match glss.Evd.it with
| [ g ] -> not (same_goal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it)
| _ -> true
let progress glss gls =
weak_progress glss gls
(* spiwack: progress normally goes like this:
(Evd.progress_evar_map gls.Evd.sigma glss.Evd.sigma) || (weak_progress glss gls)
This is immensly slow in the current implementation. Maybe we could
reimplement progress_evar_map with restricted folds like "fold_undefined",
with a good implementation of them.
*)
(* Used for congruence closure *)
let new_goal_with sigma gl extra_hyps =
let evi = Evd.find sigma gl in
let hyps = evi.Evd.evar_hyps in
let new_hyps =
List.fold_right Environ.push_named_context_val extra_hyps hyps in
let filter = evi.Evd.evar_filter in
let new_filter = Evd.Filter.extend (List.length extra_hyps) filter in
let new_evi =
{ evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in
let new_evi = Typeclasses.mark_unresolvable new_evi in
let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in
{ Evd.it = evk ; sigma = sigma; }
(* Used by the compatibility layer and typeclasses *)
let nf_evar sigma gl =
let evi = Evd.find sigma gl in
let evi = Evarutil.nf_evar_info sigma evi in
let sigma = Evd.add sigma gl evi in
(gl, sigma)
(* Goal represented as a type, doesn't take into account section variables *)
let abstract_type sigma gl =
let open EConstr in
let (gl,sigma) = nf_evar sigma gl in
let env = env sigma gl in
let genv = Global.env () in
let is_proof_var decl =
try ignore (Environ.lookup_named (NamedDecl.get_id decl) genv); false
with Not_found -> true in
Environ.fold_named_context_reverse (fun t decl ->
if is_proof_var decl then
let decl = Termops.map_named_decl EConstr.of_constr decl in
mkNamedProd_or_LetIn decl t
else
t
) ~init:(concl sigma gl) env
end
|
