1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: constrintern.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
29
let type_of_logical_kind =
35
| SubClass -> "subclass"
36
| CanonicalStructure -> "canonstruc"
41
| StructureComponent -> "proj"
42
| IdentityCoercion -> "coe"
47
| Definitional -> "defax"
49
| Conjectural -> "prfax")
60
let type_of_global_ref gr =
61
if Typeclasses.is_class gr then
66
type_of_logical_kind (Decls.constant_kind cst)
68
"var" ^ type_of_logical_kind (Decls.variable_kind v)
70
let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
71
if mib.Declarations.mind_record then
72
if mib.Declarations.mind_finite then "rec"
74
else if mib.Declarations.mind_finite then "ind"
76
| ConstructRef _ -> "constr"
78
(* To interpret implicits and arg scopes of recursive variables in
79
inductive types and recursive definitions *)
80
type var_internalisation_type = Inductive | Recursive | Method
82
type var_internalisation_data =
83
var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list
85
type implicits_env = (identifier * var_internalisation_data) list
86
type full_implicits_env = identifier list * implicits_env
88
type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
90
let interning_grammar = ref false
92
(* Historically for parsing grammar rules, but in fact used only for
93
translator, v7 parsing, and unstrict tactic internalisation *)
95
interning_grammar := true;
97
interning_grammar := false;
100
(**********************************************************************)
101
(* Internalisation errors *)
103
type internalisation_error =
104
| VariableCapture of identifier
105
| WrongExplicitImplicit
106
| IllegalMetavariable
107
| NotAConstructor of reference
108
| UnboundFixName of bool * identifier
109
| NonLinearPattern of identifier
110
| BadPatternsNumber of int * int
111
| BadExplicitationNumber of explicitation * int option
113
exception InternalisationError of loc * internalisation_error
115
let explain_variable_capture id =
116
str "The variable " ++ pr_id id ++ str " occurs in its type"
118
let explain_wrong_explicit_implicit =
119
str "Found an explicitly given implicit argument but was expecting" ++
120
fnl () ++ str "a regular one"
122
let explain_illegal_metavariable =
123
str "Metavariables allowed only in patterns"
125
let explain_not_a_constructor ref =
126
str "Unknown constructor: " ++ pr_reference ref
128
let explain_unbound_fix_name is_cofix id =
129
str "The name" ++ spc () ++ pr_id id ++
130
spc () ++ str "is not bound in the corresponding" ++ spc () ++
131
str (if is_cofix then "co" else "") ++ str "fixpoint definition"
133
let explain_non_linear_pattern id =
134
str "The variable " ++ pr_id id ++ str " is bound several times in pattern"
136
let explain_bad_patterns_number n1 n2 =
137
str "Expecting " ++ int n1 ++ str (plural n1 " pattern") ++
138
str " but found " ++ int n2
140
let explain_bad_explicitation_number n po =
142
| ExplByPos (n,_id) ->
143
let s = match po with
144
| None -> str "a regular argument"
146
str "Bad explicitation number: found " ++ int n ++
147
str" but was expecting " ++ s
149
let s = match po with
150
| None -> str "a regular argument"
151
| Some p -> (*pr_id (name_of_position p) in*) failwith "" in
152
str "Bad explicitation name: found " ++ pr_id id ++
153
str" but was expecting " ++ s
155
let explain_internalisation_error e =
156
let pp = match e with
157
| VariableCapture id -> explain_variable_capture id
158
| WrongExplicitImplicit -> explain_wrong_explicit_implicit
159
| IllegalMetavariable -> explain_illegal_metavariable
160
| NotAConstructor ref -> explain_not_a_constructor ref
161
| UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id
162
| NonLinearPattern id -> explain_non_linear_pattern id
163
| BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
164
| BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po in
167
let error_unbound_patvar loc n =
169
(loc,"glob_qualid_or_patvar", str "?" ++ pr_patvar n ++
172
let error_bad_inductive_type loc =
173
user_err_loc (loc,"",str
174
"This should be an inductive type applied to names or \"_\".")
176
let error_inductive_parameter_not_implicit loc =
177
user_err_loc (loc,"", str
178
("The parameters of inductive types do not bind in\n"^
179
"the 'return' clauses; they must be replaced by '_' in the 'in' clauses."))
181
(**********************************************************************)
182
(* Contracting "{ _ }" in notations *)
184
let rec wildcards ntn n =
185
if n = String.length ntn then []
186
else let l = spaces ntn (n+1) in if ntn.[n] = '_' then n::l else l
188
if n = String.length ntn then []
189
else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
191
let expand_notation_string ntn n =
192
let pos = List.nth (wildcards ntn 0) n in
193
let hd = if pos = 0 then "" else String.sub ntn 0 pos in
195
if pos = String.length ntn then ""
196
else String.sub ntn (pos+1) (String.length ntn - pos -1) in
199
(* This contracts the special case of "{ _ }" for sumbool, sumor notations *)
200
(* Remark: expansion of squash at definition is done in metasyntax.ml *)
201
let contract_notation ntn (l,ll) =
202
let ntn' = ref ntn in
203
let rec contract_squash n = function
205
| CNotation (_,"{ _ }",([a],[])) :: l ->
206
ntn' := expand_notation_string !ntn' n;
207
contract_squash n (a::l)
209
a::contract_squash (n+1) l in
210
let l = contract_squash 0 l in
211
(* side effect; don't inline *)
214
let contract_pat_notation ntn (l,ll) =
215
let ntn' = ref ntn in
216
let rec contract_squash n = function
218
| CPatNotation (_,"{ _ }",([a],[])) :: l ->
219
ntn' := expand_notation_string !ntn' n;
220
contract_squash n (a::l)
222
a::contract_squash (n+1) l in
223
let l = contract_squash 0 l in
224
(* side effect; don't inline *)
227
(**********************************************************************)
228
(* Remembering the parsing scope of variables in notations *)
230
let make_current_scope (tmp_scope,scopes) = Option.List.cons tmp_scope scopes
232
let set_var_scope loc id (_,_,scopt,scopes) varscopes =
233
let idscopes = List.assoc id varscopes in
234
if !idscopes <> None &
235
make_current_scope (Option.get !idscopes)
236
<> make_current_scope (scopt,scopes) then
237
user_err_loc (loc,"set_var_scope",
238
pr_id id ++ str " already occurs in a different scope.")
240
idscopes := Some (scopt,scopes)
242
(**********************************************************************)
243
(* Syntax extensions *)
245
let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env)) id =
247
(* Binders bound in the notation are considered first-order objects *)
248
let _,id' = coerce_to_id (fst (List.assoc id subst)) in
249
(renaming,(Idset.add id' ids,unb,tmpsc,scopes)), id'
251
(* Binders not bound in the notation do not capture variables *)
252
(* outside the notation (i.e. in the substitution) *)
253
let fvs1 = List.map (fun (_,(c,_)) -> free_vars_of_constr_expr c) subst in
254
let fvs2 = List.flatten (List.map (fun (_,(l,_)) -> List.map free_vars_of_constr_expr l) substlist) in
255
let fvs3 = List.map snd renaming in
256
let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in
257
let id' = next_ident_away id fvs in
258
let renaming' = if id=id' then renaming else (id,id')::renaming in
261
let rec subst_iterator y t = function
262
| RVar (_,id) as x -> if id = y then t else x
263
| x -> map_rawconstr (subst_iterator y t) x
265
let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
266
let (renaming,(ids,unb,_,scopes)) = infos in
267
let subinfos = renaming,(ids,unb,None,scopes) in
271
(* subst remembers the delimiters stack in the interpretation *)
272
(* of the notations *)
274
let (a,(scopt,subscopes)) = List.assoc id subst in
275
interp (ids,unb,scopt,subscopes@scopes) a
278
RVar (loc,List.assoc id renaming)
280
(* Happens for local notation joint with inductive/fixpoint defs *)
283
| AList (x,_,iter,terminator,lassoc) ->
285
(* All elements of the list are in scopes (scopt,subscopes) *)
286
let (l,(scopt,subscopes)) = List.assoc x substlist in
288
subst_aconstr_in_rawconstr loc interp sub subinfos terminator in
289
List.fold_right (fun a t ->
290
subst_iterator ldots_var t
291
(subst_aconstr_in_rawconstr loc interp
292
((x,(a,(scopt,subscopes)))::subst,substlist) subinfos iter))
293
(if lassoc then List.rev l else l) termin
295
anomaly "Inconsistent substitution of recursive notation")
297
rawconstr_of_aconstr_with_binders loc (traverse_binder sub)
298
(subst_aconstr_in_rawconstr loc interp sub) subinfos t
300
let intern_notation intern (_,_,tmp_scope,scopes as env) loc ntn fullargs =
301
let ntn,(args,argslist) = contract_notation ntn fullargs in
302
let (((ids,idsl),c),df) = interp_notation loc ntn (tmp_scope,scopes) in
303
Dumpglob.dump_notation_location (Topconstr.ntn_loc loc args ntn) df;
304
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
305
let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl argslist in
306
subst_aconstr_in_rawconstr loc intern (subst,substlist) ([],env) c
308
let set_type_scope (ids,unb,tmp_scope,scopes) =
309
(ids,unb,Some Notation.type_scope,scopes)
311
let reset_tmp_scope (ids,unb,tmp_scope,scopes) =
312
(ids,unb,None,scopes)
314
let rec it_mkRProd env body =
316
(na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body))
319
let rec it_mkRLambda env body =
321
(na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body))
324
(**********************************************************************)
325
(* Discriminating between bound variables and global references *)
327
(* [vars1] is a set of name to avoid (used for the tactic language);
328
[vars2] is the set of global variables, env is the set of variables
329
abstracted until this point *)
331
let string_of_ty = function
336
let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
337
let (vars1,unbndltacvars) = ltacvars in
338
(* Is [id] an inductive type potentially with implicit *)
340
let ty, l,impl,argsc = List.assoc id impls in
342
(fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
343
let tys = string_of_ty ty in
344
Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
345
RVar (loc,id), impl, argsc, l
347
(* Is [id] bound in current env or is an ltac var bound to constr *)
348
if Idset.mem id env or List.mem id vars1
350
RVar (loc,id), [], [], []
351
(* Is [id] a notation variable *)
352
else if List.mem_assoc id vars3
354
(set_var_scope loc id genv vars3; RVar (loc,id), [], [], [])
357
(* Is [id] bound to a free name in ltac (this is an ltac error message) *)
359
match List.assoc id unbndltacvars with
360
| None -> user_err_loc (loc,"intern_var",
361
str "variable " ++ pr_id id ++ str " should be bound to a term.")
362
| Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
364
(* Is [id] a goal or section variable *)
365
let _ = Sign.lookup_named id vars2 in
367
(* [id] a section variable *)
368
(* Redundant: could be done in intern_qualid *)
369
let ref = VarRef id in
370
RRef (loc, ref), implicits_of_global ref, find_arguments_scope ref, []
372
(* [id] a goal variable *)
373
RVar (loc,id), [], [], []
375
let find_appl_head_data (_,_,_,(_,impls)) = function
376
| RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
379
let error_not_enough_arguments loc =
380
user_err_loc (loc,"",str "Abbreviation is not applied enough.")
382
let check_no_explicitation l =
383
let l = List.filter (fun (a,b) -> b <> None) l in
385
let loc = fst (Option.get (snd (List.hd l))) in
387
(loc,"",str"Unexpected explicitation of the argument of an abbreviation.")
389
(* Is it a global reference or a syntactic definition? *)
390
let intern_qualid loc qid intern env args =
391
try match Nametab.extended_locate qid with
393
Dumpglob.add_glob loc ref;
394
RRef (loc, ref), args
396
Dumpglob.add_glob_kn loc sp;
397
let (ids,c) = Syntax_def.search_syntactic_definition loc sp in
398
let nids = List.length ids in
399
if List.length args < nids then error_not_enough_arguments loc;
400
let args1,args2 = list_chop nids args in
401
check_no_explicitation args1;
402
let subst = List.map2 (fun (id,scl) a -> (id,(fst a,scl))) ids args1 in
403
subst_aconstr_in_rawconstr loc intern (subst,[]) ([],env) c, args2
405
error_global_not_found_loc loc qid
407
(* Rule out section vars since these should have been found by intern_var *)
408
let intern_non_secvar_qualid loc qid intern env args =
409
match intern_qualid loc qid intern env args with
410
| RRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid
413
let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
414
| Qualid (loc, qid) ->
415
let r,args2 = intern_qualid loc qid intern env args in
416
find_appl_head_data lvar r, args2
418
try intern_var env lvar loc id, args
420
let qid = make_short_qualid id in
422
let r,args2 = intern_non_secvar_qualid loc qid intern env args in
423
find_appl_head_data lvar r, args2
425
(* Extra allowance for non globalizing functions *)
426
if !interning_grammar || unb then
427
(RVar (loc,id), [], [], []),args
430
let interp_reference vars r =
432
intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc)
433
(Idset.empty,false,None,[]) (vars,[],[],([],[])) [] r
436
let apply_scope_env (ids,unb,_,scopes) = function
437
| [] -> (ids,unb,None,scopes), []
438
| sc::scl -> (ids,unb,sc,scopes), scl
440
let rec adjust_scopes env scopes = function
443
let (enva,scopes) = apply_scope_env env scopes in
444
enva :: adjust_scopes env scopes args
446
let rec simple_adjust_scopes n = function
447
| [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
448
| sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
450
let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
451
let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
452
let npar = mib.Declarations.mind_nparams in
453
snd (list_chop (List.length pl1 + npar)
454
(simple_adjust_scopes (npar + List.length pl2)
455
(find_arguments_scope (ConstructRef cstr))))
457
(**********************************************************************)
460
let product_of_cases_patterns ids idspl =
461
List.fold_right (fun (ids,pl) (ids',ptaill) ->
463
(* Cartesian prod of the or-pats for the nth arg and the tail args *)
465
List.map (fun (subst,p) ->
466
List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl)))
469
let simple_product_of_cases_patterns pl =
470
List.fold_right (fun pl ptaill ->
471
List.flatten (List.map (fun (subst,p) ->
472
List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl))
475
(* Check linearity of pattern-matching *)
476
let rec has_duplicate = function
478
| x::l -> if List.mem x l then (Some x) else has_duplicate l
481
join_loc (fst (List.hd lhs)) (fst (list_last lhs))
483
let check_linearity lhs ids =
484
match has_duplicate ids with
486
raise (InternalisationError (loc_of_lhs lhs,NonLinearPattern id))
490
(* Match the number of pattern against the number of matched args *)
491
let check_number_of_pattern loc n l =
492
let p = List.length l in
493
if n<>p then raise (InternalisationError (loc,BadPatternsNumber (n,p)))
495
let check_or_pat_variables loc ids idsl =
496
if List.exists (fun ids' -> not (list_eq_set ids ids')) idsl then
497
user_err_loc (loc, "", str
498
"The components of this disjunctive pattern must bind the same variables.")
500
let check_constructor_length env loc cstr pl pl0 =
501
let n = List.length pl + List.length pl0 in
502
let nargs = Inductiveops.constructor_nrealargs env cstr in
503
let nhyps = Inductiveops.constructor_nrealhyps env cstr in
504
if n <> nargs && n <> nhyps (* i.e. with let's *) then
505
error_wrong_numarg_constructor_loc loc env cstr nargs
507
(* Manage multiple aliases *)
509
(* [merge_aliases] returns the sets of all aliases encountered at this
510
point and a substitution mapping extra aliases to the first one *)
511
let merge_aliases (ids,asubst as _aliases) id =
512
ids@[id], if ids=[] then asubst else (id, List.hd ids)::asubst
514
let alias_of = function
515
| ([],_) -> Anonymous
516
| (id::_,_) -> Name id
518
let message_redundant_alias (id1,id2) =
520
("Alias variable "^(string_of_id id1)^" is merged with "^(string_of_id id2))
522
(* Expanding notations *)
524
let error_invalid_pattern_notation loc =
525
user_err_loc (loc,"",str "Invalid notation for pattern.")
527
let chop_aconstr_constructor loc (ind,k) args =
528
let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
529
let params,args = list_chop nparams args in
530
List.iter (function AHole _ -> ()
531
| _ -> error_invalid_pattern_notation loc) params;
534
let rec subst_pat_iterator y t (subst,p) = match p with
535
| PatVar (_,id) as x ->
536
if id = Name y then t else [subst,x]
537
| PatCstr (loc,id,l,alias) ->
538
let l' = List.map (fun a -> (subst_pat_iterator y t ([],a))) l in
539
let pl = simple_product_of_cases_patterns l' in
540
List.map (fun (subst',pl) -> subst'@subst,PatCstr (loc,id,pl,alias)) pl
542
let subst_cases_pattern loc alias intern fullsubst scopes a =
543
let rec aux alias (subst,substlist as fullsubst) = function
546
(* subst remembers the delimiters stack in the interpretation *)
547
(* of the notations *)
549
let (a,(scopt,subscopes)) = List.assoc id subst in
550
intern (subscopes@scopes) ([],[]) scopt a
552
if id = ldots_var then [], [[], PatVar (loc,Name id)] else
553
anomaly ("Unbound pattern notation variable: "^(string_of_id id))
555
(* Happens for local notation joint with inductive/fixpoint defs *)
556
if aliases <> ([],[]) then
557
anomaly "Pattern notation without constructors";
558
[[id],[]], PatVar (loc,Name id)
561
| ARef (ConstructRef c) ->
562
([],[[], PatCstr (loc,c, [], alias)])
563
| AApp (ARef (ConstructRef cstr),args) ->
564
let args = chop_aconstr_constructor loc cstr args in
565
let idslpll = List.map (aux Anonymous fullsubst) args in
566
let ids',pll = product_of_cases_patterns [] idslpll in
567
let pl' = List.map (fun (asubst,pl) ->
568
asubst,PatCstr (loc,cstr,pl,alias)) pll in
570
| AList (x,_,iter,terminator,lassoc) ->
572
(* All elements of the list are in scopes (scopt,subscopes) *)
573
let (l,(scopt,subscopes)) = List.assoc x substlist in
574
let termin = aux Anonymous fullsubst terminator in
576
List.fold_right (fun a (tids,t) ->
577
let uids,u = aux Anonymous ((x,(a,(scopt,subscopes)))::subst,substlist) iter in
578
let pll = List.map (subst_pat_iterator ldots_var t) u in
579
tids@uids, List.flatten pll)
580
(if lassoc then List.rev l else l) termin in
581
idsl, List.map (fun ((asubst, pl) as x) ->
582
match pl with PatCstr (loc, c, pl, Anonymous) -> (asubst, PatCstr (loc, c, pl, alias)) | _ -> x) v
584
anomaly "Inconsistent substitution of recursive notation")
585
| t -> error_invalid_pattern_notation loc
586
in aux alias fullsubst a
588
(* Differentiating between constructors and matching variables *)
589
type pattern_qualid_kind =
590
| ConstrPat of constructor * (identifier list *
591
((identifier * identifier) list * cases_pattern) list) list
592
| VarPat of identifier
594
let find_constructor ref f aliases pats scopes =
595
let (loc,qid) = qualid_of_reference ref in
597
try extended_locate qid
598
with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in
601
let (vars,a) = Syntax_def.search_syntactic_definition loc sp in
603
| ARef (ConstructRef cstr) ->
606
| AApp (ARef (ConstructRef cstr),args) ->
607
let args = chop_aconstr_constructor loc cstr args in
608
let nvars = List.length vars in
609
if List.length pats < nvars then error_not_enough_arguments loc;
610
let pats1,pats2 = list_chop nvars pats in
611
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in
612
let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f (subst,[]) scopes) args in
614
| _ -> raise Not_found)
617
let rec unf = function
619
let v = Environ.constant_value (Global.env()) cst in
620
unf (global_of_constr v)
621
| ConstructRef cstr ->
622
Dumpglob.add_glob loc r;
624
| _ -> raise Not_found
627
let find_pattern_variable = function
628
| Ident (loc,id) -> id
629
| Qualid (loc,_) as x -> raise (InternalisationError(loc,NotAConstructor x))
631
let maybe_constructor ref f aliases scopes =
633
let c,idspl1,pl2 = find_constructor ref f aliases [] scopes in
637
(* patt var does not exists globally *)
638
| InternalisationError _ -> VarPat (find_pattern_variable ref)
639
(* patt var also exists globally but does not satisfy preconditions *)
640
| (Environ.NotEvaluableConst _ | Not_found) ->
641
if_verbose msg_warning (str "pattern " ++ pr_reference ref ++
642
str " is understood as a pattern variable");
643
VarPat (find_pattern_variable ref)
645
let mustbe_constructor loc ref f aliases patl scopes =
646
try find_constructor ref f aliases patl scopes
647
with (Environ.NotEvaluableConst _ | Not_found) ->
648
raise (InternalisationError (loc,NotAConstructor ref))
650
let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
651
let intern_pat = intern_cases_pattern genv in
653
| CPatAlias (loc, p, id) ->
654
let aliases' = merge_aliases aliases id in
655
intern_pat scopes aliases' tmp_scope p
656
| CPatCstr (loc, head, pl) ->
657
let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl scopes in
658
check_constructor_length genv loc c idslpl1 pl2;
659
let argscs2 = find_remaining_constructor_scopes idslpl1 pl2 c in
660
let idslpl2 = List.map2 (intern_pat scopes ([],[])) argscs2 pl2 in
661
let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in
662
let pl' = List.map (fun (asubst,pl) ->
663
(asubst, PatCstr (loc,c,pl,alias_of aliases))) pll in
665
| CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]))
666
when Bigint.is_strictly_pos p ->
667
intern_pat scopes aliases tmp_scope (CPatPrim(loc,Numeral(Bigint.neg p)))
668
| CPatNotation (_,"( _ )",([a],[])) ->
669
intern_pat scopes aliases tmp_scope a
670
| CPatNotation (loc, ntn, fullargs) ->
671
let ntn,(args,argsl) = contract_pat_notation ntn fullargs in
672
let (((ids',idsl'),c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
673
Dumpglob.dump_notation_location (Topconstr.patntn_loc loc args ntn) df;
674
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
675
let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in
677
subst_cases_pattern loc (alias_of aliases) intern_pat (subst,substlist)
680
| CPatPrim (loc, p) ->
681
let a = alias_of aliases in
682
let (c,df) = Notation.interp_prim_token_cases_pattern loc p a
683
(tmp_scope,scopes) in
684
Dumpglob.dump_notation_location (fst (unloc loc)) df;
686
| CPatDelimiters (loc, key, e) ->
687
intern_pat (find_delimiters_scope loc key::scopes) aliases None e
688
| CPatAtom (loc, Some head) ->
689
(match maybe_constructor head intern_pat aliases scopes with
690
| ConstrPat (c,idspl) ->
691
check_constructor_length genv loc c idspl [];
692
let (ids',pll) = product_of_cases_patterns ids idspl in
693
(ids,List.map (fun (asubst,pl) ->
694
(asubst, PatCstr (loc,c,pl,alias_of aliases))) pll)
696
let ids,asubst = merge_aliases aliases id in
697
(ids,[asubst, PatVar (loc,alias_of (ids,asubst))]))
698
| CPatAtom (loc, None) ->
699
(ids,[asubst, PatVar (loc,alias_of aliases)])
700
| CPatOr (loc, pl) ->
702
let pl' = List.map (intern_pat scopes aliases tmp_scope) pl in
703
let (idsl,pl') = List.split pl' in
704
let ids = List.hd idsl in
705
check_or_pat_variables loc ids (List.tl idsl);
706
(ids,List.flatten pl')
708
(**********************************************************************)
711
(**********************************************************************)
712
(* Utilities for binders *)
714
let check_capture loc ty = function
715
| Name id when occur_var_constr_expr id ty ->
716
raise (InternalisationError (loc,VariableCapture id))
720
let locate_if_isevar loc na = function
723
| Name id -> Reserve.find_reserved_type id
724
| Anonymous -> raise Not_found
725
with Not_found -> RHole (loc, Evd.BinderType na))
728
let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
729
if List.mem id indnames then
730
errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++
731
pr_id id ++ strbrk " must not be used as a bound variable in the type \
732
of its constructor.")
734
let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function
736
if fail_anonymous then errorlabstrm "" (str "Anonymous variables not allowed");
739
check_hidden_implicit_parameters id lvar;
740
(Idset.add id ids, unb,tmpsc,scopes)
742
let push_loc_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) loc = function
744
if fail_anonymous then user_err_loc (loc,"", str "Anonymous variables not allowed");
747
check_hidden_implicit_parameters id lvar;
748
Dumpglob.dump_binding loc id;
749
(Idset.add id ids,unb,tmpsc,scopes)
751
let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar
752
(ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty =
755
Implicit_quantifiers.implicit_application ids
756
Implicit_quantifiers.combine_params_freevar ty
758
let ty' = intern_type (ids,true,tmpsc,sc) ty in
759
let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids ty' in
760
let env' = List.fold_left (fun env (x, l) -> push_loc_name_env ~fail_anonymous lvar env l (Name x)) env fvs in
761
let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in
762
let na = match na with
764
if fail_anonymous then na
769
| CApp (_, (_, CRef (Ident (loc,id))), _) -> id
770
| _ -> id_of_string "H"
771
in Implicit_quantifiers.make_fresh ids (Global.env ()) id
774
in (push_loc_name_env ~fail_anonymous lvar env' loc na), (na,b',None,ty') :: List.rev bl
776
let intern_local_binder_aux ?(fail_anonymous=false) intern intern_type lvar ((ids,unb,ts,sc as env),bl) = function
777
| LocalRawAssum(nal,bk,ty) ->
780
let (loc,na) = List.hd nal in
781
(* TODO: fail if several names with different implicit types *)
782
let ty = locate_if_isevar loc na (intern_type env ty) in
784
(fun ((ids,unb,ts,sc),bl) (_,na) ->
785
((name_fold Idset.add na ids,unb,ts,sc), (na,k,None,ty)::bl))
787
| Generalized (b,b',t) ->
788
let env, b = intern_generalized_binder ~fail_anonymous intern_type lvar env bl (List.hd nal) b b' t ty in
790
| LocalRawDef((loc,na),def) ->
791
((name_fold Idset.add na ids,unb,ts,sc),
792
(na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
794
let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c =
795
let c = intern (ids,true,tmp_scope,scopes) c in
796
let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids c in
802
| None when tmp_scope = Some Notation.type_scope
803
|| List.mem Notation.type_scope scopes -> true
807
(fun (id, loc') acc ->
808
RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
810
(fun (id, loc') acc ->
811
RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
813
List.fold_right (fun (id, loc as lid) (env, acc) ->
814
let env' = push_loc_name_env lvar env loc (Name id) in
815
(env', abs lid acc)) fvs (env,c)
818
(**********************************************************************)
819
(* Utilities for application *)
821
let merge_impargs l args =
822
List.fold_right (fun a l ->
824
| (_,Some (_,(ExplByName id as x))) when
825
List.exists (function (_,Some (_,y)) -> x=y | _ -> false) args -> l
829
let check_projection isproj nargs r =
830
match (r,isproj) with
831
| RRef (loc, ref), Some _ ->
833
let n = Recordops.find_projection_nparams ref + 1 in
835
user_err_loc (loc,"",str "Projection has not the right number of explicit parameters.");
838
(loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection."))
839
| _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection.")
842
let get_implicit_name n imps =
843
Some (Impargs.name_of_implicit (List.nth imps (n-1)))
845
let set_hole_implicit i = function
846
| RRef (loc,r) -> (loc,Evd.ImplicitArg (r,i))
847
| RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i))
848
| _ -> anomaly "Only refs have implicits"
850
let exists_implicit_name id =
851
List.exists (fun imp -> is_status_implicit imp & id = name_of_implicit imp)
853
let extract_explicit_arg imps args =
854
let rec aux = function
857
let (eargs,rargs) = aux l in
859
| None -> (eargs,a::rargs)
861
let id = match pos with
863
if not (exists_implicit_name id imps) then
865
(loc,"",str "Wrong argument name: " ++ pr_id id ++ str ".");
866
if List.mem_assoc id eargs then
867
user_err_loc (loc,"",str "Argument name " ++ pr_id id
868
++ str " occurs more than once.");
870
| ExplByPos (p,_id) ->
873
let imp = List.nth imps (p-1) in
874
if not (is_status_implicit imp) then failwith "imp";
876
with Failure _ (* "nth" | "imp" *) ->
878
(loc,"",str"Wrong argument position: " ++ int p ++ str ".")
880
if List.mem_assoc id eargs then
881
user_err_loc (loc,"",str"Argument at position " ++ int p ++
882
str " is mentioned more than once.");
884
((id,(loc,a))::eargs,rargs)
887
(**********************************************************************)
890
let internalise sigma globalenv env allow_patvar lvar c =
891
let rec intern (ids,unb,tmp_scope,scopes as env) = function
893
let (c,imp,subscopes,l),_ =
894
intern_applied_reference intern env lvar [] ref in
895
(match intern_impargs c env imp subscopes l with
897
| l -> RApp (constr_loc x, c, l))
898
| CFix (loc, (locid,iddef), dl) ->
899
let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
900
let dl = Array.of_list dl in
902
try list_index0 iddef lf
904
raise (InternalisationError (locid,UnboundFixName (false,iddef)))
907
(fun (id,(n,order),bl,ty,bd) ->
908
let intern_ro_arg c f =
911
Some (loc, n) -> list_index0 (Name n) (List.map snd (names_of_local_assums bl))
914
let before, after = list_chop idx bl in
915
let ((ids',_,_,_) as env',rbefore) =
916
List.fold_left intern_local_binder (env,[]) before in
920
| Some c' -> f (intern (ids', unb, tmp_scope, scopes) c')
922
let n' = Option.map (fun _ -> List.length before) n in
923
n', ro, List.fold_left intern_local_binder (env',rbefore) after
925
let n, ro, ((ids',_,_,_),rbl) =
928
intern_ro_arg None (fun _ -> RStructRec)
930
intern_ro_arg (Some c) (fun r -> RWfRec r)
932
intern_ro_arg (Some c) (fun r -> RMeasureRec r))
934
let ids'' = List.fold_right Idset.add lf ids' in
935
((n, ro), List.rev rbl,
936
intern_type (ids',unb,tmp_scope,scopes) ty,
937
intern (ids'',unb,None,scopes) bd)) dl in
939
(Array.map (fun (ro,_,_,_) -> ro) idl,n),
941
Array.map (fun (_,bl,_,_) -> bl) idl,
942
Array.map (fun (_,_,ty,_) -> ty) idl,
943
Array.map (fun (_,_,_,bd) -> bd) idl)
944
| CCoFix (loc, (locid,iddef), dl) ->
945
let lf = List.map (fun ((_, id),_,_,_) -> id) dl in
946
let dl = Array.of_list dl in
948
try list_index0 iddef lf
950
raise (InternalisationError (locid,UnboundFixName (true,iddef)))
953
(fun (id,bl,ty,bd) ->
954
let ((ids',_,_,_),rbl) =
955
List.fold_left intern_local_binder (env,[]) bl in
956
let ids'' = List.fold_right Idset.add lf ids' in
958
intern_type (ids',unb,tmp_scope,scopes) ty,
959
intern (ids'',unb,None,scopes) bd)) dl in
962
Array.map (fun (bl,_,_) -> bl) idl,
963
Array.map (fun (_,ty,_) -> ty) idl,
964
Array.map (fun (_,_,bd) -> bd) idl)
965
| CArrow (loc,c1,c2) ->
966
RProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2)
967
| CProdN (loc,[],c2) ->
969
| CProdN (loc,(nal,bk,ty)::bll,c2) ->
970
iterate_prod loc env bk ty (CProdN (loc, bll, c2)) nal
971
| CLambdaN (loc,[],c2) ->
973
| CLambdaN (loc,(nal,bk,ty)::bll,c2) ->
974
iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal
975
| CLetIn (loc,(loc1,na),c1,c2) ->
976
RLetIn (loc, na, intern (reset_tmp_scope env) c1,
977
intern (push_loc_name_env lvar env loc1 na) c2)
978
| CNotation (loc,"- _",([CPrim (_,Numeral p)],[]))
979
when Bigint.is_strictly_pos p ->
980
intern env (CPrim (loc,Numeral (Bigint.neg p)))
981
| CNotation (_,"( _ )",([a],[])) -> intern env a
982
| CNotation (loc,ntn,args) ->
983
intern_notation intern env loc ntn args
984
| CGeneralization (loc,b,a,c) ->
985
intern_generalization intern env lvar loc b a c
987
let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in
988
Dumpglob.dump_notation_location (fst (unloc loc)) df;
990
| CDelimiters (loc, key, e) ->
991
intern (ids,unb,None,find_delimiters_scope loc key::scopes) e
992
| CAppExpl (loc, (isproj,ref), args) ->
993
let (f,_,args_scopes,_),args =
994
let args = List.map (fun a -> (a,None)) args in
995
intern_applied_reference intern env lvar args ref in
996
check_projection isproj (List.length args) f;
997
RApp (loc, f, intern_args env args_scopes (List.map fst args))
998
| CApp (loc, (isproj,f), args) ->
999
let isproj,f,args = match f with
1000
(* Compact notations like "t.(f args') args" *)
1001
| CApp (_,(Some _,f), args') when isproj=None -> isproj,f,args'@args
1002
(* Don't compact "(f args') args" to resolve implicits separately *)
1003
| _ -> isproj,f,args in
1004
let (c,impargs,args_scopes,l),args =
1006
| CRef ref -> intern_applied_reference intern env lvar args ref
1007
| CNotation (loc,ntn,([],[])) ->
1008
let c = intern_notation intern env loc ntn ([],[]) in
1009
find_appl_head_data lvar c, args
1010
| x -> (intern env f,[],[],[]), args in
1012
intern_impargs c env impargs args_scopes (merge_impargs l args) in
1013
check_projection isproj (List.length args) c;
1015
(* Now compact "(f args') args" *)
1016
| RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
1017
| _ -> RApp (loc, c, args))
1018
| CRecord (loc, w, fs) ->
1019
let id, _ = List.hd fs in
1021
let (id,_,_,_),_ = intern_applied_reference intern env lvar [] (Ident id) in
1023
| RRef (loc, ref) ->
1024
(try Recordops.find_projection ref
1025
with Not_found -> user_err_loc (loc, "intern", str"Not a projection"))
1026
| c -> user_err_loc (loc_of_rawconstr id, "intern", str"Not a projection")
1029
let pars = list_make record.Recordops.s_EXPECTEDPARAM (CHole (loc, None)) in
1031
List.fold_left (fun (args, rest as acc) (na, b) ->
1034
let id = out_name na in
1035
let _, t = List.assoc id rest in
1036
t :: args, List.remove_assoc id rest
1037
with _ -> CHole (loc, Some (Evd.QuestionMark (Evd.Define true))) :: args, rest
1038
else acc) ([], List.map (fun ((loc, id), t) -> id, (loc, t)) fs) record.Recordops.s_PROJKIND
1041
let id, (loc, t) = List.hd rest in
1042
user_err_loc (loc,"intern",(str "Unknown field name " ++ pr_id id))
1043
else pars @ List.rev fields
1046
Qualid (loc, shortest_qualid_of_global Idset.empty (ConstructRef record.Recordops.s_CONST))
1048
let app = CAppExpl (loc, (None, constrname), args) in
1051
| CCases (loc, sty, rtnpo, tms, eqns) ->
1052
let tms,env' = List.fold_right
1053
(fun citm (inds,env) ->
1054
let (tm,ind),nal = intern_case_item env citm in
1055
(tm,ind)::inds,List.fold_left (push_name_env lvar) env nal)
1057
let rtnpo = Option.map (intern_type env') rtnpo in
1058
let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
1059
RCases (loc, sty, rtnpo, tms, List.flatten eqns')
1060
| CLetTuple (loc, nal, (na,po), b, c) ->
1061
let env' = reset_tmp_scope env in
1062
let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
1063
let env'' = List.fold_left (push_name_env lvar) env ids in
1064
let p' = Option.map (intern_type env'') po in
1065
RLetTuple (loc, nal, (na', p'), b',
1066
intern (List.fold_left (push_name_env lvar) env nal) c)
1067
| CIf (loc, c, (na,po), b1, b2) ->
1068
let env' = reset_tmp_scope env in
1069
let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
1070
let env'' = List.fold_left (push_name_env lvar) env ids in
1071
let p' = Option.map (intern_type env'') po in
1072
RIf (loc, c', (na', p'), intern env b1, intern env b2)
1074
RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true))
1075
| CPatVar (loc, n) when allow_patvar ->
1077
| CPatVar (loc, _) ->
1078
raise (InternalisationError (loc,IllegalMetavariable))
1079
| CEvar (loc, n, l) ->
1080
REvar (loc, n, Option.map (List.map (intern env)) l)
1083
| CCast (loc, c1, CastConv (k, c2)) ->
1084
RCast (loc,intern env c1, CastConv (k, intern_type env c2))
1085
| CCast (loc, c1, CastCoerce) ->
1086
RCast (loc,intern env c1, CastCoerce)
1088
| CDynamic (loc,d) -> RDynamic (loc,d)
1090
and intern_type env = intern (set_type_scope env)
1092
and intern_local_binder env bind =
1093
intern_local_binder_aux intern intern_type lvar env bind
1095
(* Expands a multiple pattern into a disjunction of multiple patterns *)
1096
and intern_multiple_pattern scopes n (loc,pl) =
1098
List.map (intern_cases_pattern globalenv scopes ([],[]) None) pl in
1099
check_number_of_pattern loc n pl;
1100
product_of_cases_patterns [] idsl_pll
1102
(* Expands a disjunction of multiple pattern *)
1103
and intern_disjunctive_multiple_pattern scopes loc n mpl =
1105
let mpl' = List.map (intern_multiple_pattern scopes n) mpl in
1106
let (idsl,mpl') = List.split mpl' in
1107
let ids = List.hd idsl in
1108
check_or_pat_variables loc ids (List.tl idsl);
1109
(ids,List.flatten mpl')
1111
(* Expands a pattern-matching clause [lhs => rhs] *)
1112
and intern_eqn n (ids,unb,tmp_scope,scopes) (loc,lhs,rhs) =
1113
let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc n lhs in
1114
(* Linearity implies the order in ids is irrelevant *)
1115
check_linearity lhs eqn_ids;
1116
let env_ids = List.fold_right Idset.add eqn_ids ids in
1117
List.map (fun (asubst,pl) ->
1118
let rhs = replace_vars_constr_expr asubst rhs in
1119
List.iter message_redundant_alias asubst;
1120
let rhs' = intern (env_ids,unb,tmp_scope,scopes) rhs in
1121
(loc,eqn_ids,pl,rhs')) pll
1123
and intern_case_item (vars,unb,_,scopes as env) (tm,(na,t)) =
1124
let tm' = intern env tm in
1125
let ids,typ = match t with
1127
let tids = ids_of_cases_indtype t in
1128
let tids = List.fold_right Idset.add tids Idset.empty in
1129
let t = intern_type (tids,unb,None,scopes) t in
1130
let loc,ind,l = match t with
1131
| RRef (loc,IndRef ind) -> (loc,ind,[])
1132
| RApp (loc,RRef (_,IndRef ind),l) -> (loc,ind,l)
1133
| _ -> error_bad_inductive_type (loc_of_rawconstr t) in
1134
let nparams, nrealargs = inductive_nargs globalenv ind in
1135
let nindargs = nparams + nrealargs in
1136
if List.length l <> nindargs then
1137
error_wrong_numarg_inductive_loc loc globalenv ind nindargs;
1138
let nal = List.map (function
1139
| RHole loc -> Anonymous
1140
| RVar (_,id) -> Name id
1141
| c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name.")) l in
1142
let parnal,realnal = list_chop nparams nal in
1143
if List.exists ((<>) Anonymous) parnal then
1144
error_inductive_parameter_not_implicit loc;
1145
realnal, Some (loc,ind,nparams,realnal)
1148
let na = match tm', na with
1149
| RVar (_,id), None when Idset.mem id vars -> Name id
1150
| _, None -> Anonymous
1151
| _, Some na -> na in
1152
(tm',(na,typ)), na::ids
1154
and iterate_prod loc2 env bk ty body nal =
1155
let rec default env bk = function
1157
if nal <> [] then check_capture loc1 ty na;
1158
let body = default (push_loc_name_env lvar env loc1 na) bk nal in
1159
let ty = locate_if_isevar loc1 na (intern_type env ty) in
1160
RProd (join_loc loc1 loc2, na, bk, ty, body)
1161
| [] -> intern_type env body
1164
| Default b -> default env b nal
1165
| Generalized (b,b',t) ->
1166
let env, ibind = intern_generalized_binder intern_type lvar
1167
env [] (List.hd nal) b b' t ty in
1168
let body = intern_type env body in
1169
it_mkRProd ibind body
1171
and iterate_lam loc2 env bk ty body nal =
1172
let rec default env bk = function
1174
if nal <> [] then check_capture loc1 ty na;
1175
let body = default (push_loc_name_env lvar env loc1 na) bk nal in
1176
let ty = locate_if_isevar loc1 na (intern_type env ty) in
1177
RLambda (join_loc loc1 loc2, na, bk, ty, body)
1178
| [] -> intern env body
1180
| Default b -> default env b nal
1181
| Generalized (b, b', t) ->
1182
let env, ibind = intern_generalized_binder intern_type lvar
1183
env [] (List.hd nal) b b' t ty in
1184
let body = intern env body in
1185
it_mkRLambda ibind body
1187
and intern_impargs c env l subscopes args =
1188
let eargs, rargs = extract_explicit_arg l args in
1189
let rec aux n impl subscopes eargs rargs =
1190
let (enva,subscopes') = apply_scope_env env subscopes in
1191
match (impl,rargs) with
1192
| (imp::impl', rargs) when is_status_implicit imp ->
1194
let id = name_of_implicit imp in
1195
let (_,a) = List.assoc id eargs in
1196
let eargs' = List.remove_assoc id eargs in
1197
intern enva a :: aux (n+1) impl' subscopes' eargs' rargs
1199
if rargs=[] & eargs=[] & not (maximal_insertion_of imp) then
1200
(* Less regular arguments than expected: complete *)
1201
(* with implicit arguments if maximal insertion is set *)
1204
RHole (set_hole_implicit (n,get_implicit_name n l) c) ::
1205
aux (n+1) impl' subscopes' eargs rargs
1207
| (imp::impl', a::rargs') ->
1208
intern enva a :: aux (n+1) impl' subscopes' eargs rargs'
1209
| (imp::impl', []) ->
1211
(let (id,(loc,_)) = List.hd eargs in
1212
user_err_loc (loc,"",str "Not enough non implicit
1213
arguments to accept the argument bound to " ++
1214
pr_id id ++ str"."));
1217
assert (eargs = []);
1218
intern_args env subscopes rargs
1219
in aux 1 l subscopes eargs rargs
1221
and intern_args env subscopes = function
1224
let (enva,subscopes) = apply_scope_env env subscopes in
1225
(intern enva a) :: (intern_args env subscopes args)
1231
InternalisationError (loc,e) ->
1232
user_err_loc (loc,"internalize",explain_internalisation_error e)
1234
(**************************************************************************)
1235
(* Functions to translate constr_expr into rawconstr *)
1236
(**************************************************************************)
1238
let extract_ids env =
1239
List.fold_right Idset.add
1240
(Termops.ids_of_rel_context (Environ.rel_context env))
1243
let intern_gen isarity sigma env
1244
?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
1247
if isarity then Some Notation.type_scope else None in
1248
internalise sigma env (extract_ids env, false, tmp_scope,[])
1249
allow_patvar (ltacvars,Environ.named_context env, [], impls) c
1251
let intern_constr sigma env c = intern_gen false sigma env c
1253
let intern_type sigma env c = intern_gen true sigma env c
1255
let intern_pattern env patt =
1257
intern_cases_pattern env [] ([],[]) None patt
1259
InternalisationError (loc,e) ->
1260
user_err_loc (loc,"internalize",explain_internalisation_error e)
1263
let intern_ltac isarity ltacvars sigma env c =
1264
intern_gen isarity sigma env ~ltacvars:ltacvars c
1266
type manual_implicits = (explicitation * (bool * bool)) list
1268
(*********************************************************************)
1269
(* Functions to parse and interpret constructions *)
1271
let interp_gen kind sigma env
1272
?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
1274
let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in
1275
Default.understand_gen kind sigma env c
1277
let interp_constr sigma env c =
1278
interp_gen (OfType None) sigma env c
1280
let interp_type sigma env ?(impls=([],[])) c =
1281
interp_gen IsType sigma env ~impls c
1283
let interp_casted_constr sigma env ?(impls=([],[])) c typ =
1284
interp_gen (OfType (Some typ)) sigma env ~impls c
1286
let interp_open_constr sigma env c =
1287
Default.understand_tcc sigma env (intern_constr sigma env c)
1289
let interp_constr_judgment sigma env c =
1290
Default.understand_judgment sigma env (intern_constr sigma env c)
1292
let interp_constr_evars_gen_impls ?evdref
1293
env ?(impls=([],[])) kind c =
1296
let c = intern_gen (kind=IsType) ~impls Evd.empty env c in
1297
let imps = Implicit_quantifiers.implicits_of_rawterm c in
1298
Default.understand_gen kind Evd.empty env c, imps
1300
let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
1301
let imps = Implicit_quantifiers.implicits_of_rawterm c in
1302
Default.understand_tcc_evars evdref env kind c, imps
1304
let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
1305
let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
1306
Default.understand_tcc_evars evdref env kind c
1308
let interp_casted_constr_evars_impls ?evdref
1309
env ?(impls=([],[])) c typ =
1310
interp_constr_evars_gen_impls ?evdref env ~impls (OfType (Some typ)) c
1312
let interp_type_evars_impls ?evdref env ?(impls=([],[])) c =
1313
interp_constr_evars_gen_impls ?evdref env IsType ~impls c
1315
let interp_constr_evars_impls ?evdref env ?(impls=([],[])) c =
1316
interp_constr_evars_gen_impls ?evdref env (OfType None) ~impls c
1318
let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
1319
interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
1321
let interp_type_evars evdref env ?(impls=([],[])) c =
1322
interp_constr_evars_gen evdref env IsType ~impls c
1324
let interp_constr_judgment_evars evdref env c =
1325
Default.understand_judgment_tcc evdref env
1326
(intern_constr (Evd.evars_of !evdref) env c)
1328
type ltac_sign = identifier list * unbound_ltac_var_map
1330
let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
1331
let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in
1332
pattern_of_rawconstr c
1334
let interp_aconstr impls (vars,varslist) a =
1335
let env = Global.env () in
1336
(* [vl] is intended to remember the scope of the free variables of [a] *)
1337
let vl = List.map (fun id -> (id,ref None)) (vars@varslist) in
1338
let c = internalise Evd.empty (Global.env()) (extract_ids env, false, None, [])
1339
false (([],[]),Environ.named_context env,vl,([],impls)) a in
1340
(* Translate and check that [c] has all its free variables bound in [vars] *)
1341
let a = aconstr_of_rawconstr vars c in
1342
(* Returns [a] and the ordered list of variables with their scopes *)
1343
(* Variables occurring in binders have no relevant scope since bound *)
1344
let vl = List.map (fun (id,r) ->
1345
(id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl in
1346
list_chop (List.length vars) vl, a
1348
(* Interpret binders and contexts *)
1350
let interp_binder sigma env na t =
1351
let t = intern_gen true sigma env t in
1352
let t' = locate_if_isevar (loc_of_rawconstr t) na t in
1353
Default.understand_type sigma env t'
1355
let interp_binder_evars evdref env na t =
1356
let t = intern_gen true (Evd.evars_of !evdref) env t in
1357
let t' = locate_if_isevar (loc_of_rawconstr t) na t in
1358
Default.understand_tcc_evars evdref env IsType t'
1363
let my_intern_constr sigma env lvar acc c =
1364
internalise sigma env acc false lvar c
1366
let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c
1368
let intern_context fail_anonymous sigma env params =
1369
let lvar = (([],[]),Environ.named_context env, [], ([], [])) in
1371
(intern_local_binder_aux ~fail_anonymous (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
1372
((extract_ids env,false,None,[]), []) params)
1374
let interp_context_gen understand_type understand_judgment env bl =
1375
let (env, par, _, impls) =
1377
(fun (env,params,n,impls) (na, k, b, t) ->
1380
let t' = locate_if_isevar (loc_of_rawconstr t) na t in
1381
let t = understand_type env t' in
1382
let d = (na,None,t) in
1384
if k = Implicit then
1385
let na = match na with Name n -> Some n | Anonymous -> None in
1386
(ExplByPos (n, na), (true, true)) :: impls
1389
(push_rel d env, d::params, succ n, impls)
1391
let c = understand_judgment env b in
1392
let d = (na, Some c.uj_val, c.uj_type) in
1393
(push_rel d env, d::params, succ n, impls))
1394
(env,[],1,[]) (List.rev bl)
1395
in (env, par), impls
1397
let interp_context ?(fail_anonymous=false) sigma env params =
1398
let bl = intern_context fail_anonymous sigma env params in
1399
interp_context_gen (Default.understand_type sigma)
1400
(Default.understand_judgment sigma) env bl
1402
let interp_context_evars ?(fail_anonymous=false) evdref env params =
1403
let bl = intern_context fail_anonymous (Evd.evars_of !evdref) env params in
1404
interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
1405
(Default.understand_judgment_tcc evdref) env bl
1407
(**********************************************************************)
1408
(* Locating reference, possibly via an abbreviation *)
1410
let locate_reference qid =
1411
match Nametab.extended_locate qid with
1412
| TrueGlobal ref -> ref
1413
| SyntacticDef kn ->
1414
match Syntax_def.search_syntactic_definition dummy_loc kn with
1415
| [],ARef ref -> ref
1416
| _ -> raise Not_found
1420
let _ = locate_reference (make_short_qualid id) in true
1424
let global_reference id =
1425
constr_of_global (locate_reference (make_short_qualid id))
1427
let construct_reference ctx id =
1429
Term.mkVar (let _ = Sign.lookup_named id ctx in id)
1433
let global_reference_in_absolute_module dir id =
1434
constr_of_global (Nametab.absolute_reference (Libnames.make_path dir id))
added
removed
interp/constrintern.ml
