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: constrextern.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
33
(* Translation from rawconstr to front constr *)
35
(**********************************************************************)
38
(* This governs printing of local context of references *)
39
let print_arguments = ref false
41
(* If true, prints local context of evars, whatever print_arguments *)
42
let print_evar_arguments = ref false
44
(* This governs printing of implicit arguments. When
45
[print_implicits] is on then [print_implicits_explicit_args] tells
46
how implicit args are printed. If on, implicit args are printed
47
with the form (id:=arg) otherwise arguments are printed normally and
48
the function is prefixed by "@" *)
49
let print_implicits = ref false
50
let print_implicits_explicit_args = ref false
52
(* Tells if implicit arguments not known to be inferable from a rigid
53
position are systematically printed *)
54
let print_implicits_defensive = ref true
56
(* This forces printing of coercions *)
57
let print_coercions = ref false
59
(* This forces printing universe names of Type{.} *)
60
let print_universes = ref false
62
(* This suppresses printing of primitive tokens (e.g. numeral) and symbols *)
63
let print_no_symbol = ref false
65
(* This governs printing of projections using the dot notation symbols *)
66
let print_projections = ref false
68
let print_meta_as_hole = ref false
70
let with_arguments f = Flags.with_option print_arguments f
71
let with_implicits f = Flags.with_option print_implicits f
72
let with_coercions f = Flags.with_option print_coercions f
73
let with_universes f = Flags.with_option print_universes f
74
let without_symbols f = Flags.with_option print_no_symbol f
75
let with_meta_as_hole f = Flags.with_option print_meta_as_hole f
77
(**********************************************************************)
78
(* Various externalisation functions *)
80
let insert_delimiters e = function
82
| Some sc -> CDelimiters (dummy_loc,sc,e)
84
let insert_pat_delimiters loc p = function
86
| Some sc -> CPatDelimiters (loc,sc,p)
88
let insert_pat_alias loc p = function
90
| Name id -> CPatAlias (loc,p,id)
92
(**********************************************************************)
93
(* conversion of references *)
95
let ids_of_ctxt ctxt =
98
(function c -> match kind_of_term c with
101
error "Arbitrary substitution of references not implemented.")
104
let idopt_of_name = function
108
let extern_evar loc n l =
109
if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None)
111
let debug_global_reference_printer =
112
ref (fun _ -> failwith "Cannot print a global reference")
114
let set_debug_global_reference_printer f =
115
debug_global_reference_printer := f
117
let extern_reference loc vars r =
118
try Qualid (loc,shortest_qualid_of_global vars r)
120
(* happens in debugger *)
121
!debug_global_reference_printer loc r
123
(************************************************************************)
124
(* Equality up to location (useful for translator v8) *)
126
let rec check_same_pattern p1 p2 =
128
| CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) when i1=i2 ->
129
check_same_pattern a1 a2
130
| CPatCstr(_,c1,a1), CPatCstr(_,c2,a2) when c1=c2 ->
131
List.iter2 check_same_pattern a1 a2
132
| CPatAtom(_,r1), CPatAtom(_,r2) when r1=r2 -> ()
133
| CPatPrim(_,i1), CPatPrim(_,i2) when i1=i2 -> ()
134
| CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 ->
135
check_same_pattern e1 e2
136
| _ -> failwith "not same pattern"
138
let check_same_ref r1 r2 =
140
| Qualid(_,q1), Qualid(_,q2) when q1=q2 -> ()
141
| Ident(_,i1), Ident(_,i2) when i1=i2 -> ()
142
| _ -> failwith "not same ref"
144
let rec check_same_type ty1 ty2 =
146
| CRef r1, CRef r2 -> check_same_ref r1 r2
147
| CFix(_,(_,id1),fl1), CFix(_,(_,id2),fl2) when id1=id2 ->
148
List.iter2 (fun (id1,i1,bl1,a1,b1) (id2,i2,bl2,a2,b2) ->
149
if id1<>id2 || i1<>i2 then failwith "not same fix";
150
check_same_fix_binder bl1 bl2;
151
check_same_type a1 a2;
152
check_same_type b1 b2)
154
| CCoFix(_,(_,id1),fl1), CCoFix(_,(_,id2),fl2) when id1=id2 ->
155
List.iter2 (fun (id1,bl1,a1,b1) (id2,bl2,a2,b2) ->
156
if id1<>id2 then failwith "not same fix";
157
check_same_fix_binder bl1 bl2;
158
check_same_type a1 a2;
159
check_same_type b1 b2)
161
| CArrow(_,a1,b1), CArrow(_,a2,b2) ->
162
check_same_type a1 a2;
163
check_same_type b1 b2
164
| CProdN(_,bl1,a1), CProdN(_,bl2,a2) ->
165
List.iter2 check_same_binder bl1 bl2;
166
check_same_type a1 a2
167
| CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) ->
168
List.iter2 check_same_binder bl1 bl2;
169
check_same_type a1 a2
170
| CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when na1=na2 ->
171
check_same_type a1 a2;
172
check_same_type b1 b2
173
| CAppExpl(_,r1,al1), CAppExpl(_,r2,al2) when r1=r2 ->
174
List.iter2 check_same_type al1 al2
175
| CApp(_,(_,e1),al1), CApp(_,(_,e2),al2) ->
176
check_same_type e1 e2;
177
List.iter2 (fun (a1,e1) (a2,e2) ->
178
if e1<>e2 then failwith "not same expl";
179
check_same_type a1 a2) al1 al2
180
| CCases(_,_,_,a1,brl1), CCases(_,_,_,a2,brl2) ->
181
List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2;
182
List.iter2 (fun (_,pl1,r1) (_,pl2,r2) ->
183
List.iter2 (located_iter2 (List.iter2 check_same_pattern)) pl1 pl2;
184
check_same_type r1 r2) brl1 brl2
185
| CHole _, CHole _ -> ()
186
| CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> ()
187
| CSort(_,s1), CSort(_,s2) when s1=s2 -> ()
188
| CCast(_,a1,CastConv (_,b1)), CCast(_,a2, CastConv(_,b2)) ->
189
check_same_type a1 a2;
190
check_same_type b1 b2
191
| CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) ->
192
check_same_type a1 a2
193
| CNotation(_,n1,(e1,el1)), CNotation(_,n2,(e2,el2)) when n1=n2 ->
194
List.iter2 check_same_type e1 e2;
195
List.iter2 (List.iter2 check_same_type) el1 el2
196
| CPrim(_,i1), CPrim(_,i2) when i1=i2 -> ()
197
| CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 ->
198
check_same_type e1 e2
199
| _ when ty1=ty2 -> ()
200
| _ -> failwith "not same type"
202
and check_same_binder (nal1,_,e1) (nal2,_,e2) =
203
List.iter2 (fun (_,na1) (_,na2) ->
204
if na1<>na2 then failwith "not same name") nal1 nal2;
205
check_same_type e1 e2
207
and check_same_fix_binder bl1 bl2 =
208
List.iter2 (fun b1 b2 ->
210
LocalRawAssum(nal1,k,ty1), LocalRawAssum(nal2,k',ty2) ->
211
check_same_binder (nal1,k,ty1) (nal2,k',ty2)
212
| LocalRawDef(na1,def1), LocalRawDef(na2,def2) ->
213
check_same_binder ([na1],default_binder_kind,def1) ([na2],default_binder_kind,def2)
214
| _ -> failwith "not same binder") bl1 bl2
216
let same c d = try check_same_type c d; true with _ -> false
218
(* Idem for rawconstr *)
220
let array_iter2 f v1 v2 =
221
List.iter2 f (Array.to_list v1) (Array.to_list v2)
223
let rec same_patt p1 p2 =
225
PatVar(_,na1), PatVar(_,na2) -> if na1<>na2 then failwith "PatVar"
226
| PatCstr(_,c1,pl1,al1), PatCstr(_,c2,pl2,al2) ->
227
if c1<>c2 || al1 <> al2 then failwith "PatCstr";
228
List.iter2 same_patt pl1 pl2
229
| _ -> failwith "same_patt"
231
let rec same_raw c d =
233
| RRef(_,gr1), RRef(_,gr2) -> if gr1<>gr2 then failwith "RRef"
234
| RVar(_,id1), RVar(_,id2) -> if id1<>id2 then failwith "RVar"
235
| REvar(_,e1,a1), REvar(_,e2,a2) ->
236
if e1 <> e2 then failwith "REvar";
237
Option.iter2(List.iter2 same_raw) a1 a2
238
| RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar"
239
| RApp(_,f1,a1), RApp(_,f2,a2) ->
240
List.iter2 same_raw (f1::a1) (f2::a2)
241
| RLambda(_,na1,bk1,t1,m1), RLambda(_,na2,bk2,t2,m2) ->
242
if na1 <> na2 then failwith "RLambda";
243
same_raw t1 t2; same_raw m1 m2
244
| RProd(_,na1,bk1,t1,m1), RProd(_,na2,bk2,t2,m2) ->
245
if na1 <> na2 then failwith "RProd";
246
same_raw t1 t2; same_raw m1 m2
247
| RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) ->
248
if na1 <> na2 then failwith "RLetIn";
249
same_raw t1 t2; same_raw m1 m2
250
| RCases(_,_,_,c1,b1), RCases(_,_,_,c2,b2) ->
252
(fun (t1,(al1,oind1)) (t2,(al2,oind2)) ->
254
if al1 <> al2 then failwith "RCases";
255
Option.iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) ->
256
if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2;
257
List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) ->
258
List.iter2 same_patt pl1 pl2;
259
same_raw b1 b2) b1 b2
260
| RLetTuple(_,nl1,_,b1,c1), RLetTuple(_,nl2,_,b2,c2) ->
261
if nl1<>nl2 then failwith "RLetTuple";
264
| RIf(_,b1,_,t1,e1),RIf(_,b2,_,t2,e2) ->
265
same_raw b1 b2; same_raw t1 t2; same_raw e1 e2
266
| RRec(_,fk1,na1,bl1,ty1,def1), RRec(_,fk2,na2,bl2,ty2,def2) ->
267
if fk1 <> fk2 || na1 <> na2 then failwith "RRec";
269
(List.iter2 (fun (na1,bk1,bd1,ty1) (na2,bk2,bd2,ty2) ->
270
if na1<>na2 then failwith "RRec";
271
Option.iter2 same_raw bd1 bd2;
272
same_raw ty1 ty2)) bl1 bl2;
273
array_iter2 same_raw ty1 ty2;
274
array_iter2 same_raw def1 def2
275
| RSort(_,s1), RSort(_,s2) -> if s1<>s2 then failwith "RSort"
278
| RCast(_,c1,_),r2 -> same_raw c1 r2
279
| r1, RCast(_,c2,_) -> same_raw r1 c2
280
| RDynamic(_,d1), RDynamic(_,d2) -> if d1<>d2 then failwith"RDynamic"
281
| _ -> failwith "same_raw"
283
let same_rawconstr c d =
284
try same_raw c d; true
285
with Failure _ | Invalid_argument _ -> false
287
(**********************************************************************)
288
(* mapping patterns to cases_pattern_expr *)
290
let has_curly_brackets ntn =
291
String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or
292
String.sub ntn (String.length ntn - 6) 6 = " { _ }" or
293
string_string_contains ntn " { _ } ")
295
let rec wildcards ntn n =
296
if n = String.length ntn then []
297
else let l = spaces ntn (n+1) in if ntn.[n] = '_' then n::l else l
299
if n = String.length ntn then []
300
else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
302
let expand_curly_brackets loc mknot ntn (l,ll) =
303
let ntn' = ref ntn in
304
let rec expand_ntn i =
309
let p = List.nth (wildcards !ntn' 0) i - 2 in
310
if p>=0 & p+5 <= String.length !ntn' & String.sub !ntn' p 5 = "{ _ }"
313
String.sub !ntn' 0 p ^ "_" ^
314
String.sub !ntn' (p+5) (String.length !ntn' -p-5);
315
mknot (loc,"{ _ }",([a],[])) end
317
a' :: expand_ntn (i+1) l in
318
let l = expand_ntn 0 l in
320
mknot (loc,!ntn',(l,ll))
322
let destPrim = function CPrim(_,t) -> Some t | _ -> None
323
let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
325
let make_notation_gen loc ntn mknot mkprim destprim l =
326
if has_curly_brackets ntn
327
then expand_curly_brackets loc mknot ntn l
328
else match ntn,List.map destprim (fst l),(snd l) with
329
(* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
330
| "- _", [Some (Numeral p)],[] when Bigint.is_strictly_pos p ->
331
mknot (loc,ntn,([mknot (loc,"( _ )",l)],[]))
333
match decompose_notation_key ntn, l with
334
| [Terminal "-"; Terminal x], ([],[]) ->
335
(try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x)))
336
with _ -> mknot (loc,ntn,([],[])))
337
| [Terminal x], ([],[]) ->
338
(try mkprim (loc, Numeral (Bigint.of_string x))
339
with _ -> mknot (loc,ntn,([],[])))
343
let make_notation loc ntn l =
344
make_notation_gen loc ntn
345
(fun (loc,ntn,l) -> CNotation (loc,ntn,l))
346
(fun (loc,p) -> CPrim (loc,p))
349
let make_pat_notation loc ntn l =
350
make_notation_gen loc ntn
351
(fun (loc,ntn,l) -> CPatNotation (loc,ntn,l))
352
(fun (loc,p) -> CPatPrim (loc,p))
355
let bind_env (sigma,sigmalist as fullsigma) var v =
357
let vvar = List.assoc var sigma in
358
if v=vvar then fullsigma else raise No_match
360
(* TODO: handle the case of multiple occs in different scopes *)
361
(var,v)::sigma,sigmalist
363
let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
364
| r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
365
| PatVar (_,Anonymous), AHole _ -> sigma
366
| a, AHole _ -> sigma
367
| PatCstr (loc,(ind,_ as r1),args1,_), _ ->
369
(fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
372
| ARef (ConstructRef r2) when r1 = r2 -> []
373
| AApp (ARef (ConstructRef r2),l2) when r1 = r2 -> l2
374
| _ -> raise No_match in
375
if List.length l2 <> nparams + List.length args1
378
let (p2,args2) = list_chop nparams l2 in
379
(* All parameters must be _ *)
380
List.iter (function AHole _ -> () | _ -> raise No_match) p2;
381
List.fold_left2 (match_cases_pattern metas) sigma args1 args2
382
(* TODO: use recursive notations *)
383
| _ -> raise No_match
385
let match_aconstr_cases_pattern c ((metas_scl,metaslist_scl),pat) =
386
let vars = List.map fst metas_scl @ List.map fst metaslist_scl in
387
let subst,substlist = match_cases_pattern vars ([],[]) c pat in
388
(* Reorder canonically the substitution *)
390
try List.assoc x subst
391
with Not_found -> anomaly "match_aconstr_cases_pattern" in
392
List.map (fun (x,scl) -> (find x subst,scl)) metas_scl,
393
List.map (fun (x,scl) -> (find x substlist,scl)) metaslist_scl
395
(* Better to use extern_rawconstr composed with injection/retraction ?? *)
396
let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
398
if !Flags.raw_print or !print_no_symbol then raise No_match;
399
let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
400
match availability_of_prim_token sc scopes with
401
| None -> raise No_match
403
let loc = cases_pattern_loc pat in
404
insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na
407
if !Flags.raw_print or !print_no_symbol then raise No_match;
408
extern_symbol_pattern scopes vars pat
409
(uninterp_cases_pattern_notations pat)
412
| PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,id)))
413
| PatVar (loc,Anonymous) -> CPatAtom (loc, None)
414
| PatCstr(loc,cstrsp,args,na) ->
415
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
417
(loc,extern_reference loc vars (ConstructRef cstrsp),args) in
418
insert_pat_alias loc p na
420
and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
421
| [] -> raise No_match
422
| (keyrule,pat,n as _rule)::rules ->
424
(* Check the number of arguments expected by the notation *)
425
let loc,na = match t,n with
426
| PatCstr (_,f,l,_), Some n when List.length l > n ->
428
| PatCstr (loc,_,_,na),_ -> loc,na
429
| PatVar (loc,na),_ -> loc,na in
430
(* Try matching ... *)
431
let subst,substlist = match_aconstr_cases_pattern t pat in
432
(* Try availability of interpretation ... *)
433
let p = match keyrule with
434
| NotationRule (sc,ntn) ->
435
(match availability_of_notation (sc,ntn) allscopes with
436
(* Uninterpretation is not allowed in current context *)
437
| None -> raise No_match
438
(* Uninterpretation is allowed in current context *)
439
| Some (scopt,key) ->
440
let scopes' = Option.List.cons scopt scopes in
442
List.map (fun (c,(scopt,scl)) ->
443
extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
446
List.map (fun (c,(scopt,scl)) ->
447
let subscope = (scopt,scl@scopes') in
448
List.map (extern_cases_pattern_in_scope subscope vars) c)
450
insert_pat_delimiters loc
451
(make_pat_notation loc ntn (l,ll)) key)
453
let qid = shortest_qualid_of_syndef vars kn in
454
CPatAtom (loc,Some (Qualid (loc, qid))) in
455
insert_pat_alias loc p na
457
No_match -> extern_symbol_pattern allscopes vars t rules
459
let extern_cases_pattern vars p =
460
extern_cases_pattern_in_scope (None,[]) vars p
462
(**********************************************************************)
463
(* Externalising applications *)
465
let occur_name na aty =
467
| Name id -> occur_var_constr_expr id aty
470
let is_projection nargs = function
471
| Some r when not !Flags.raw_print & !print_projections ->
473
let n = Recordops.find_projection_nparams r + 1 in
474
if n <= nargs then Some n else None
475
with Not_found -> None)
478
let is_hole = function CHole _ -> true | _ -> false
480
let is_significant_implicit a impl tail =
481
not (is_hole a) or (tail = [] & not (List.for_all is_status_implicit impl))
483
(* Implicit args indexes are in ascending order *)
484
(* inctx is useful only if there is a last argument to be deduced from ctxt *)
485
let explicitize loc inctx impl (cf,f) args =
486
let n = List.length args in
487
let rec exprec q = function
488
| a::args, imp::impl when is_status_implicit imp ->
489
let tail = exprec (q+1) (args,impl) in
492
(!print_implicits & !print_implicits_explicit_args) or
493
(!print_implicits_defensive &
494
is_significant_implicit a impl tail &
495
not (is_inferable_implicit inctx n imp))
498
(a,Some (dummy_loc, ExplByName (name_of_implicit imp))) :: tail
501
| a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl)
502
| args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*)
504
match is_projection (List.length args) cf with
506
if impl <> [] & is_status_implicit (List.nth impl (i-1)) then
507
let f' = match f with CRef f -> f | _ -> assert false in
508
CAppExpl (loc,(ip,f'),args)
510
let (args1,args2) = list_chop i args in
511
let (impl1,impl2) = if impl=[] then [],[] else list_chop i impl in
512
let args1 = exprec 1 (args1,impl1) in
513
let args2 = exprec (i+1) (args2,impl2) in
514
CApp (loc,(Some (List.length args1),f),args1@args2)
516
let args = exprec 1 (args,impl) in
517
if args = [] then f else CApp (loc, (None, f), args)
519
let extern_global loc impl f =
520
if impl <> [] & List.for_all is_status_implicit impl then
521
CAppExpl (loc, (None, f), [])
525
let extern_app loc inctx impl (cf,f) args =
526
if args = [] (* maybe caused by a hidden coercion *) then
527
extern_global loc impl f
530
((!Flags.raw_print or
531
(!print_implicits & not !print_implicits_explicit_args)) &
532
List.exists is_status_implicit impl)
534
CAppExpl (loc, (is_projection (List.length args) cf, f), args)
536
explicitize loc inctx impl (cf,CRef f) args
538
let rec extern_args extern scopes env args subscopes =
542
let argscopes, subscopes = match subscopes with
543
| [] -> (None,scopes), []
544
| scopt::subscopes -> (scopt,scopes), subscopes in
545
extern argscopes env a :: extern_args extern scopes env args subscopes
547
let rec remove_coercions inctx = function
548
| RApp (loc,RRef (_,r),args) as c
549
when not (!Flags.raw_print or !print_coercions)
551
let nargs = List.length args in
552
(try match Classops.hide_coercion r with
553
| Some n when n < nargs && (inctx or n+1 < nargs) ->
554
(* We skip a coercion *)
555
let l = list_skipn n args in
556
let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
557
(* Recursively remove the head coercions *)
558
(match remove_coercions true a with
559
| RApp (_,a,l') -> RApp (loc,a,l'@l)
560
| a -> RApp (loc,a,l))
565
let rec rename_rawconstr_var id0 id1 = function
566
RRef(loc,VarRef id) when id=id0 -> RRef(loc,VarRef id1)
567
| RVar(loc,id) when id=id0 -> RVar(loc,id1)
568
| c -> map_rawconstr (rename_rawconstr_var id0 id1) c
570
let rec share_fix_binders n rbl ty def =
572
RProd(_,na0,bk0,t0,b), RLambda(_,na1,bk1,t1,m) ->
573
if not(same_rawconstr t0 t1) then List.rev rbl, ty, def
577
Name id0, Name id1 ->
578
if id0=id1 then (na0,b,m)
579
else if not (occur_rawconstr id1 b) then
580
(na1,rename_rawconstr_var id0 id1 b,m)
581
else if not (occur_rawconstr id0 m) then
582
(na1,b,rename_rawconstr_var id1 id0 m)
583
else (* vraiment pas de chance! *)
584
failwith "share_fix_binders: capture"
585
| Name id, Anonymous ->
586
if not (occur_rawconstr id m) then (na0,b,m)
588
failwith "share_fix_binders: capture"
589
| Anonymous, Name id ->
590
if not (occur_rawconstr id b) then (na1,b,m)
592
failwith "share_fix_binders: capture"
594
share_fix_binders (n-1) ((na,None,t0)::rbl) b m
595
| _ -> List.rev rbl, ty, def
597
(**********************************************************************)
598
(* mapping rawterms to numerals (in presence of coercions, choose the *)
599
(* one with no delimiter if possible) *)
601
let extern_possible_prim_token scopes r =
603
let (sc,n) = uninterp_prim_token r in
604
match availability_of_prim_token sc scopes with
606
| Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key)
610
let extern_optimal_prim_token scopes r r' =
611
let c = extern_possible_prim_token scopes r in
612
let c' = if r==r' then None else extern_possible_prim_token scopes r' in
614
| Some n, (Some (CDelimiters _) | None) | _, Some n -> n
615
| _ -> raise No_match
617
(**********************************************************************)
618
(* mapping rawterms to constr_expr *)
620
let extern_rawsort = function
622
| RType (Some _) as s when !print_universes -> s
623
| RType _ -> RType None
625
let rec extern inctx scopes vars r =
626
let r' = remove_coercions inctx r in
628
if !Flags.raw_print or !print_no_symbol then raise No_match;
629
extern_optimal_prim_token scopes r r'
632
if !Flags.raw_print or !print_no_symbol then raise No_match;
633
extern_symbol scopes vars r' (uninterp_notations r')
634
with No_match -> match r' with
636
extern_global loc (implicits_of_global ref)
637
(extern_reference loc vars ref)
639
| RVar (loc,id) -> CRef (Ident (loc,id))
641
| REvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None)
644
extern_evar loc n (Option.map (List.map (extern false scopes vars)) l)
647
if !print_meta_as_hole then CHole (loc, None) else CPatVar (loc,n)
649
| RApp (loc,f,args) ->
652
let subscopes = find_arguments_scope ref in
654
extern_args (extern true) (snd scopes) vars args subscopes in
655
extern_app loc inctx (implicits_of_global ref)
656
(Some ref,extern_reference rloc vars ref)
659
explicitize loc inctx [] (None,sub_extern false scopes vars f)
660
(List.map (sub_extern true scopes vars) args))
662
| RProd (loc,Anonymous,_,t,c) ->
663
(* Anonymous product are never factorized *)
664
CArrow (loc,extern_typ scopes vars t, extern_typ scopes vars c)
666
| RLetIn (loc,na,t,c) ->
667
CLetIn (loc,(loc,na),sub_extern false scopes vars t,
668
extern inctx scopes (add_vname vars na) c)
670
| RProd (loc,na,bk,t,c) ->
671
let t = extern_typ scopes vars (anonymize_if_reserved na t) in
672
let (idl,c) = factorize_prod scopes (add_vname vars na) t c in
673
CProdN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
675
| RLambda (loc,na,bk,t,c) ->
676
let t = extern_typ scopes vars (anonymize_if_reserved na t) in
677
let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
678
CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
680
| RCases (loc,sty,rtntypopt,tml,eqns) ->
682
List.fold_right (name_fold Idset.add)
683
(cases_predicate_names tml) vars in
684
let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
685
let tml = List.map (fun (tm,(na,x)) ->
686
let na' = match na,tm with
687
Anonymous, RVar (_,id) when
688
rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt)
690
| Anonymous, _ -> None
691
| Name id, RVar (_,id') when id=id' -> None
692
| Name _, _ -> Some na in
693
(sub_extern false scopes vars tm,
694
(na',Option.map (fun (loc,ind,n,nal) ->
695
let params = list_tabulate
696
(fun _ -> RHole (dummy_loc,Evd.InternalHole)) n in
697
let args = List.map (function
698
| Anonymous -> RHole (dummy_loc,Evd.InternalHole)
699
| Name id -> RVar (dummy_loc,id)) nal in
700
let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in
701
(extern_typ scopes vars t)) x))) tml in
702
let eqns = List.map (extern_eqn inctx scopes vars) eqns in
703
CCases (loc,sty,rtntypopt',tml,eqns)
705
| RLetTuple (loc,nal,(na,typopt),tm,b) ->
707
(Option.map (fun _ -> na) typopt,
708
Option.map (extern_typ scopes (add_vname vars na)) typopt),
709
sub_extern false scopes vars tm,
710
extern inctx scopes (List.fold_left add_vname vars nal) b)
712
| RIf (loc,c,(na,typopt),b1,b2) ->
713
CIf (loc,sub_extern false scopes vars c,
714
(Option.map (fun _ -> na) typopt,
715
Option.map (extern_typ scopes (add_vname vars na)) typopt),
716
sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
718
| RRec (loc,fk,idv,blv,tyv,bv) ->
719
let vars' = Array.fold_right Idset.add idv vars in
723
Array.mapi (fun i fi ->
724
let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
725
let (ids,bl) = extern_local_binder scopes vars bl in
726
let vars0 = List.fold_right (name_fold Idset.add) ids vars in
727
let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
729
match fst nv.(i) with
731
| Some x -> Some (dummy_loc, out_name (List.nth ids x))
733
let ro = extern_recursion_order scopes vars (snd nv.(i)) in
734
((dummy_loc, fi), (n, ro), bl, extern_typ scopes vars0 ty,
735
extern false scopes vars1 def)) idv
737
CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
740
Array.mapi (fun i fi ->
741
let (ids,bl) = extern_local_binder scopes vars blv.(i) in
742
let vars0 = List.fold_right (name_fold Idset.add) ids vars in
743
let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
744
((dummy_loc, fi),bl,extern_typ scopes vars0 tyv.(i),
745
sub_extern false scopes vars1 bv.(i))) idv
747
CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
749
| RSort (loc,s) -> CSort (loc,extern_rawsort s)
751
| RHole (loc,e) -> CHole (loc, Some e)
753
| RCast (loc,c, CastConv (k,t)) ->
754
CCast (loc,sub_extern true scopes vars c, CastConv (k,extern_typ scopes vars t))
755
| RCast (loc,c, CastCoerce) ->
756
CCast (loc,sub_extern true scopes vars c, CastCoerce)
758
| RDynamic (loc,d) -> CDynamic (loc,d)
760
and extern_typ (_,scopes) =
761
extern true (Some Notation.type_scope,scopes)
763
and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
765
and factorize_prod scopes vars aty c =
767
if !Flags.raw_print or !print_no_symbol then raise No_match;
768
([],extern_symbol scopes vars c (uninterp_notations c))
769
with No_match -> match c with
770
| RProd (loc,(Name id as na),bk,ty,c)
771
when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
772
& not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *)
773
-> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in
774
((loc,Name id)::nal,c)
775
| c -> ([],extern_typ scopes vars c)
777
and factorize_lambda inctx scopes vars aty c =
779
if !Flags.raw_print or !print_no_symbol then raise No_match;
780
([],extern_symbol scopes vars c (uninterp_notations c))
781
with No_match -> match c with
782
| RLambda (loc,na,bk,ty,c)
783
when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
784
& not (occur_name na aty) (* To avoid na in ty' escapes scope *)
786
factorize_lambda inctx scopes (add_vname vars na) aty c in
788
| c -> ([],sub_extern inctx scopes vars c)
790
and extern_local_binder scopes vars = function
792
| (na,bk,Some bd,ty)::l ->
794
extern_local_binder scopes (name_fold Idset.add na vars) l in
796
LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l)
798
| (na,bk,None,ty)::l ->
799
let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in
800
(match extern_local_binder scopes (name_fold Idset.add na vars) l with
801
(ids,LocalRawAssum(nal,k,ty')::l)
803
match na with Name id -> not (occur_var_constr_expr id ty')
806
LocalRawAssum((dummy_loc,na)::nal,k,ty')::l)
809
LocalRawAssum([(dummy_loc,na)],Default bk,ty) :: l))
811
and extern_eqn inctx scopes vars (loc,ids,pl,c) =
812
(loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
813
extern inctx scopes vars c)
815
and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
816
| [] -> raise No_match
817
| (keyrule,pat,n as _rule)::rules ->
818
let loc = Rawterm.loc_of_rawconstr t in
820
(* Adjusts to the number of arguments expected by the notation *)
821
let (t,args) = match t,n with
822
| RApp (_,(RRef _ as f),args), Some n when List.length args >= n ->
823
let args1, args2 = list_chop n args in
824
(if n = 0 then f else RApp (dummy_loc,f,args1)), args2
825
| RApp (_,(RRef _ as f),args), None -> f, args
826
| RRef _, Some 0 -> RApp (dummy_loc,t,[]), []
828
| _ -> raise No_match in
829
(* Try matching ... *)
830
let subst,substlist = match_aconstr t pat in
831
(* Try availability of interpretation ... *)
834
| NotationRule (sc,ntn) ->
835
(match availability_of_notation (sc,ntn) allscopes with
836
(* Uninterpretation is not allowed in current context *)
837
| None -> raise No_match
838
(* Uninterpretation is allowed in current context *)
839
| Some (scopt,key) ->
840
let scopes' = Option.List.cons scopt scopes in
842
List.map (fun (c,(scopt,scl)) ->
843
extern (* assuming no overloading: *) true
844
(scopt,scl@scopes') vars c)
847
List.map (fun (c,(scopt,scl)) ->
848
List.map (extern true (scopt,scl@scopes') vars) c)
850
insert_delimiters (make_notation loc ntn (l,ll)) key)
853
List.map (fun (c,(scopt,scl)) ->
854
extern true (scopt,scl@scopes) vars c, None)
856
let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in
857
if l = [] then a else CApp (loc,(None,a),l) in
860
(* TODO: compute scopt for the extra args, in case, head is a ref *)
861
explicitize loc false [] (None,e)
862
(List.map (extern true allscopes vars) args)
864
No_match -> extern_symbol allscopes vars t rules
866
and extern_recursion_order scopes vars = function
867
RStructRec -> CStructRec
868
| RWfRec c -> CWfRec (extern true scopes vars c)
869
| RMeasureRec c -> CMeasureRec (extern true scopes vars c)
872
let extern_rawconstr vars c =
873
extern false (None,[]) vars c
875
let extern_rawtype vars c =
876
extern_typ (None,[]) vars c
878
(******************************************************************)
879
(* Main translation function from constr -> constr_expr *)
881
let loc = dummy_loc (* for constr and pattern, locations are lost *)
883
let extern_constr_gen at_top scopt env t =
884
let avoid = if at_top then ids_of_context env else [] in
885
let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
886
let vars = vars_of_env env in
887
extern false (scopt,[]) vars r
889
let extern_constr_in_scope at_top scope env t =
890
extern_constr_gen at_top (Some scope) env t
892
let extern_constr at_top env t =
893
extern_constr_gen at_top None env t
895
let extern_type at_top env t =
896
let avoid = if at_top then ids_of_context env else [] in
897
let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
898
extern_rawtype (vars_of_env env) r
900
let extern_sort s = extern_rawsort (detype_sort s)
902
(******************************************************************)
903
(* Main translation function from pattern -> constr_expr *)
905
let it_destPLambda n c =
906
let rec aux n nal c =
907
if n=0 then (nal,c) else match c with
908
| PLambda (na,_,c) -> aux (n-1) (na::nal) c
909
| _ -> anomaly "it_destPLambda" in
912
let rec raw_of_pat env = function
913
| PRef ref -> RRef (loc,ref)
914
| PVar id -> RVar (loc,id)
915
| PEvar (n,l) -> REvar (loc,n,Some (array_map_to_list (raw_of_pat env) l))
917
let id = try match lookup_name_of_rel n env with
920
anomaly "rawconstr_of_pattern: index to an anonymous variable"
921
with Not_found -> id_of_string ("_UNBOUND_REL_"^(string_of_int n)) in
923
| PMeta None -> RHole (loc,Evd.InternalHole)
924
| PMeta (Some n) -> RPatVar (loc,(false,n))
926
RApp (loc,raw_of_pat env f,array_map_to_list (raw_of_pat env) args)
928
RApp (loc,RPatVar (loc,(true,n)),
929
List.map (raw_of_pat env) args)
931
RProd (loc,na,Explicit,raw_of_pat env t,raw_of_pat (na::env) c)
933
RLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
934
| PLambda (na,t,c) ->
935
RLambda (loc,na,Explicit,raw_of_pat env t, raw_of_pat (na::env) c)
937
RIf (loc, raw_of_pat env c, (Anonymous,None),
938
raw_of_pat env b1, raw_of_pat env b2)
939
| PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) ->
940
let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in
941
RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b)
942
| PCase (_,PMeta None,tm,[||]) ->
943
RCases (loc,RegularStyle,None,[raw_of_pat env tm,(Anonymous,None)],[])
944
| PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) ->
945
let brs = Array.to_list (Array.map (raw_of_pat env) bv) in
946
let brns = Array.to_list cstr_nargs in
947
(* ind is None only if no branch and no return type *)
948
let ind = Option.get indo in
949
let mat = simple_cases_matrix_of_branches ind brns brs in
951
if p = PMeta None then (Anonymous,None),None
953
let nparams,n = Option.get ind_nargs in
954
return_type_of_predicate ind nparams n (raw_of_pat env p) in
955
RCases (loc,RegularStyle,rtn,[raw_of_pat env tm,indnames],mat)
956
| PFix f -> Detyping.detype false [] env (mkFix f)
957
| PCoFix c -> Detyping.detype false [] env (mkCoFix c)
958
| PSort s -> RSort (loc,s)
960
and raw_of_eqns env constructs consnargsl bl =
961
Array.to_list (array_map3 (raw_of_eqn env) constructs consnargsl bl)
963
and raw_of_eqn env constr construct_nargs branch =
964
let make_pat x env b ids =
965
let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
966
let id = next_name_away_with_default "x" x avoid in
967
PatVar (dummy_loc,Name id),(Name id)::env,id::ids
969
let rec buildrec ids patlist env n b =
972
[PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
977
let pat,new_env,new_ids = make_pat x env b ids in
978
buildrec new_ids (pat::patlist) new_env (n-1) b
981
let pat,new_env,new_ids = make_pat x env b ids in
982
buildrec new_ids (pat::patlist) new_env (n-1) b
985
error "Unsupported branch in case-analysis while printing pattern."
987
buildrec [] [] env construct_nargs branch
989
let extern_constr_pattern env pat =
990
extern true (None,[]) Idset.empty (raw_of_pat env pat)
992
let extern_rel_context where env sign =
993
let a = detype_rel_context where [] (names_of_rel_context env) sign in
994
let vars = vars_of_env env in
995
snd (extern_local_binder (None,[]) vars a)
added
removed
interp/constrextern.ml
