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
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
open Pretyping
open Evd
open Environ
open Term
open Rawterm
open Topconstr
open Names
open Libnames
open Pp
open Vernacexpr
open Constrintern
open Subtac_command
open Typeclasses
open Typeclasses_errors
open Termops
open Decl_kinds
open Entries
open Util
module SPretyping = Subtac_pretyping.Pretyping
let interp_binder_evars evdref env na t =
let t = Constrintern.intern_gen true (Evd.evars_of !evdref) env t in
SPretyping.understand_tcc_evars evdref env IsType t
let interp_binders_evars isevars env avoid l =
List.fold_left
(fun (env, ids, params) ((loc, i), t) ->
let n = Name i in
let t' = interp_binder_evars isevars env n t in
let d = (i,None,t') in
(push_named d env, i :: ids, d::params))
(env, avoid, []) l
let interp_typeclass_context_evars isevars env avoid l =
List.fold_left
(fun (env, ids, params) (iid, bk, cl) ->
let t' = interp_binder_evars isevars env (snd iid) cl in
let i = match snd iid with
| Anonymous -> Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids
| Name id -> id
in
let d = (i,None,t') in
(push_named d env, i :: ids, d::params))
(env, avoid, []) l
let interp_constrs_evars isevars env avoid l =
List.fold_left
(fun (env, ids, params) t ->
let t' = interp_binder_evars isevars env Anonymous t in
let id = Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids in
let d = (id,None,t') in
(push_named d env, id :: ids, d::params))
(env, avoid, []) l
let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
SPretyping.understand_tcc_evars evdref env kind
(intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c)
let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
let type_ctx_instance isevars env ctx inst subst =
List.fold_left2
(fun (subst, instctx) (na, _, t) ce ->
let t' = replace_vars subst t in
let c = interp_casted_constr_evars isevars env ce t' in
let d = na, Some c, t' in
(na, c) :: subst, d :: instctx)
(subst, []) (List.rev ctx) inst
let type_class_instance_params isevars env id n ctx inst subst =
List.fold_left2
(fun (subst, instctx) (na, _, t) ce ->
let t' = replace_vars subst t in
let c =
(* if ce = CHole (dummy_loc) then *)
(* (\* Control over the evars which are direct superclasses to avoid partial instanciations *)
(* in instance search. *\) *)
(* Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t' *)
(* else *)
interp_casted_constr_evars isevars env ce t'
in
let d = na, Some c, t' in
(na, c) :: subst, d :: instctx)
(subst, []) (List.rev ctx) inst
let substitution_of_constrs ctx cstrs =
List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx []
let new_instance sup (instid, bk, cl) props =
let id, par = Implicit_quantifiers.destClassAppExpl cl in
let env = Global.env() in
let isevars = ref (Evd.create_evar_defs Evd.empty) in
let avoid = Termops.ids_of_context env in
let k =
try class_info (snd id)
with Not_found -> unbound_class env id
in
let gen_ctx, sup = Implicit_quantifiers.resolve_class_binders (vars_of_env env) sup in
let gen_ctx =
let is_free ((_, x), _) =
let f l = not (List.exists (fun ((_, y), _) -> y = x) l) in
let g l = not (List.exists (fun ((_, y), _, _) -> y = Name x) l) in
f gen_ctx && g sup
in
let parbinders = Implicit_quantifiers.compute_constrs_freevars_binders (vars_of_env env) (List.map fst par) in
let parbinders' = List.filter is_free parbinders in
gen_ctx @ parbinders'
in
let env', avoid, genctx = interp_binders_evars isevars env avoid gen_ctx in
let env', avoid, supctx = interp_typeclass_context_evars isevars env' avoid sup in
let subst =
let cl_context = List.map snd k.cl_context in
match bk with
| Explicit ->
let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
let needlen = List.fold_left (fun acc (x, y) -> if x = None then succ acc else acc) 0 k.cl_context in
if needlen <> applen then
Classes.mismatched_params env (List.map fst par) cl_context;
let pars, _ = Implicit_quantifiers.combine_params Idset.empty (* need no avoid *)
(fun avoid (clname, (id, _, t)) ->
match clname with
Some _ -> CHole (Util.dummy_loc), avoid
| None -> failwith ("new instance: under-applied typeclass"))
par (List.rev k.cl_context)
in
let subst, _ = type_class_instance_params isevars env' (snd id) 0 cl_context pars [] in
subst
| Implicit ->
let t' = interp_type_evars isevars env' (Topconstr.CApp (Util.dummy_loc, (None, CRef (Ident id)), par)) in
match kind_of_term t' with
App (c, args) ->
substitution_of_constrs cl_context
(List.rev (Array.to_list args))
| _ -> assert false
in
isevars := Evarutil.nf_evar_defs !isevars;
let sigma = Evd.evars_of !isevars in
isevars := resolve_typeclasses ~check:false env sigma !isevars;
let sigma = Evd.evars_of !isevars in
let substctx = Typeclasses.nf_substitution sigma subst in
let subst, _propsctx =
let props =
List.map (fun (x, l, d) ->
x, Topconstr.abstract_constr_expr d (Classes.binders_of_lidents l))
props
in
if List.length props > List.length k.cl_props then
Classes.mismatched_props env' (List.map snd props) k.cl_props;
let props, rest =
List.fold_left
(fun (props, rest) (id,_,_) ->
try
let (_, c) = List.find (fun ((_,id'), c) -> id' = id) rest in
let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
c :: props, rest'
with Not_found -> (CHole Util.dummy_loc :: props), rest)
([], props) k.cl_props
in
if rest <> [] then
unbound_method env k.cl_name (fst (List.hd rest))
else
type_ctx_instance isevars env' k.cl_props props substctx
in
let app =
applistc (mkConstruct (k.cl_impl, 1)) (List.rev_map snd subst)
in
let term = it_mkNamedLambda_or_LetIn (it_mkNamedLambda_or_LetIn app supctx) genctx in
isevars := Evarutil.nf_evar_defs !isevars;
let term = Evarutil.nf_isevar !isevars term in
let termtype =
let app = applistc (mkInd (k.cl_impl)) (List.rev_map snd substctx) in
let t = it_mkNamedProd_or_LetIn (it_mkNamedProd_or_LetIn app supctx) genctx in
Evarutil.nf_isevar !isevars t
in
isevars := undefined_evars !isevars;
let id =
match snd instid with
Name id -> id
| Anonymous ->
let i = Nameops.add_suffix (snd id) "_instance_" in
Termops.next_global_ident_away false i (Termops.ids_of_context env)
in
let imps =
Util.list_map_i
(fun i (na, b, t) -> ExplByPos (i, Some na), (true, true))
1 (genctx @ List.rev supctx)
in
let hook cst =
let inst =
{ is_class = k;
is_name = id;
(* is_params = paramsctx; *)
(* is_super = superctx; *)
is_impl = cst;
(* is_add_hint = (fun () -> Classes.add_instance_hint id); *)
}
in
Classes.add_instance_hint id;
Impargs.declare_manual_implicits false (ConstRef cst) false imps;
Typeclasses.add_instance inst
in
let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
ignore (Subtac_obligations.add_definition id constr typ ~kind:Instance ~hook obls)
|
