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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id$ *)
open Pp
open Util
open Names
open Nameops
open Term
open Termops
open Sign
open Environ
open Evd
open Proof_type
open Refiner
open Proof_trees
open Logic
open Reductionops
open Tacmach
open Evar_refiner
open Rawterm
open Pattern
open Tacexpr
open Clenv
let clenv_wtactic wt clenv =
{ templval = clenv.templval;
templtyp = clenv.templtyp;
namenv = clenv.namenv;
env = clenv.env;
hook = wt clenv.hook }
(* This function put casts around metavariables whose type could not be
* infered by the refiner, that is head of applications, predicates and
* subject of Cases.
* Does check that the casted type is closed. Anyway, the refiner would
* fail in this case... *)
let clenv_cast_meta clenv =
let rec crec u =
match kind_of_term u with
| App _ | Case _ -> crec_hd u
| Cast (c,_) when isMeta c -> u
| _ -> map_constr crec u
and crec_hd u =
match kind_of_term (strip_outer_cast u) with
| Meta mv ->
(try
match Metamap.find mv clenv.env with
| Cltyp b ->
let b' = clenv_instance clenv b in
if occur_meta b' then u else mkCast (mkMeta mv, b')
| Clval(_) -> u
with Not_found ->
u)
| App(f,args) -> mkApp (crec_hd f, Array.map crec args)
| Case(ci,p,c,br) ->
mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
| _ -> u
in
crec
let clenv_refine kONT clenv gls =
tclTHEN
(kONT clenv.hook)
(refine (clenv_instance_template clenv)) gls
let clenv_refine_cast kONT clenv gls =
tclTHEN
(kONT clenv.hook)
(refine (clenv_cast_meta clenv (clenv_instance_template clenv)))
gls
let res_pf kONT clenv gls =
clenv_refine kONT (clenv_unique_resolver false clenv gls) gls
let res_pf_cast kONT clenv gls =
clenv_refine_cast kONT (clenv_unique_resolver false clenv gls) gls
let elim_res_pf kONT clenv allow_K gls =
clenv_refine_cast kONT (clenv_unique_resolver allow_K clenv gls) gls
let elim_res_pf_THEN_i kONT clenv tac gls =
let clenv' = (clenv_unique_resolver true clenv gls) in
tclTHENLASTn (clenv_refine kONT clenv') (tac clenv') gls
(* [clenv_pose_dependent_evars clenv]
* For each dependent evar in the clause-env which does not have a value,
* pose a value for it by constructing a fresh evar. We do this in
* left-to-right order, so that every evar's type is always closed w.r.t.
* metas. *)
let clenv_pose_dependent_evars clenv =
let dep_mvs = clenv_dependent false clenv in
List.fold_left
(fun clenv mv ->
let evar = Evarutil.new_evar_in_sign (w_env clenv.hook) in
let (evar_n,_) = destEvar evar in
let tY = clenv_instance_type clenv mv in
let clenv' = clenv_wtactic (w_Declare evar_n tY) clenv in
clenv_assign mv evar clenv')
clenv
dep_mvs
let e_res_pf kONT clenv gls =
clenv_refine kONT
(clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)) gls
(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
particulier ne semblent pas vérifier que des instances différentes
d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
let unifyTerms m n gls =
let env = pf_env gls in
let sigma = project gls in
tclIDTAC {it = gls.it;
sigma = fst (Unification.w_unify false env CONV m n (sigma,Evd.Metamap.empty))}
let unify m gls =
let n = pf_concl gls in unifyTerms m n gls
|
