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: ppconstr.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
27
let sep_p = fun _ -> str"."
28
let sep_v = fun _ -> str"," ++ spc()
29
let sep_pp = fun _ -> str":"
30
let sep_bar = fun _ -> spc() ++ str"| "
31
let pr_tight_coma () = str "," ++ cut ()
46
let lnegint = 35 (* must be consistent with Notation "- x" *)
51
let prec_less child (parent,assoc) =
52
if parent < 0 && child = lprod then true
54
let parent = abs parent in
56
| E -> (<=) child parent
57
| L -> (<) child parent
61
let prec_of_prim_token = function
62
| Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint
67
let print_hunks n pr (env,envlist) unp =
68
let env = ref env and envlist = ref envlist in
69
let pop r = let a = List.hd !r in r := List.tl !r; a in
70
let rec aux = function
72
| UnpMetaVar (_,prec) :: l ->
73
let c = pop env in pr (n,prec) c ++ aux l
74
| UnpListMetaVar (_,prec,sl) :: l ->
75
let cl = pop envlist in
76
let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in
79
| UnpTerminal s :: l -> str s ++ aux l
80
| UnpBox (b,sub) :: l ->
81
(* Keep order: side-effects *)
82
let pp1 = ppcmd_of_box b (aux sub) in
85
| UnpCut cut :: l -> ppcmd_of_cut cut ++ aux l in
88
let pr_notation pr s env =
89
let unpl, level = find_notation_printing_rule s in
90
print_hunks level pr env unpl, level
92
let pr_delimiters key strm =
95
let pr_generalization bk ak c =
98
| Implicit -> "{", "}"
99
| Explicit -> "(", ")"
100
in (* TODO: syntax Abstraction Kind *)
101
str "`" ++ str hd ++ c ++ str tl
104
if Flags.do_beautify() && n <> 0 then comment n
107
let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
109
let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
111
let pr_optc pr = function
113
| Some x -> pr_sep_com spc pr x
115
let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
117
let pr_universe = Univ.pr_uni
119
let pr_rawsort = function
120
| RProp Term.Null -> str "Prop"
121
| RProp Term.Pos -> str "Set"
122
| RType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment pr_universe) u)
125
let pr_name = pr_name
126
let pr_qualid = pr_qualid
128
let pr_expl_args pr (a,expl) =
130
| None -> pr (lapp,L) a
131
| Some (_,ExplByPos (n,_id)) ->
132
anomaly("Explicitation by position not implemented")
133
| Some (_,ExplByName id) ->
134
str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
136
let pr_opt_type pr = function
138
| t -> cut () ++ str ":" ++ pr t
140
let pr_opt_type_spc pr = function
142
| t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
144
let pr_lident (loc,id) =
145
if loc <> dummy_loc then
146
let (b,_) = unloc loc in
147
pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
150
let pr_lname = function
151
(loc,Name id) -> pr_lident (loc,id)
152
| lna -> pr_located pr_name lna
154
let pr_or_var pr = function
156
| ArgVar (loc,s) -> pr_lident (loc,s)
158
let pr_prim_token = function
159
| Numeral n -> Bigint.pr_bigint n
163
hov 0 (str (Evd.string_of_existential n) ++
166
spc () ++ pr_in_comment
168
str"[" ++ hov 0 (prlist_with_sep pr_coma (pr ltop) l) ++ str"]")
175
let rec pr_patt sep inh p =
176
let (strm,prec) = match p with
177
| CPatAlias (_,p,id) ->
178
pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las
179
| CPatCstr (_,c,[]) -> pr_reference c, latom
180
| CPatCstr (_,c,args) ->
181
pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
182
| CPatAtom (_,None) -> str "_", latom
183
| CPatAtom (_,Some r) -> pr_reference r, latom
185
hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator
186
| CPatNotation (_,"( _ )",([p],[])) ->
187
pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
188
| CPatNotation (_,s,env) -> pr_notation (pr_patt mt) s env
189
| CPatPrim (_,p) -> pr_prim_token p, latom
190
| CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
192
let loc = cases_pattern_expr_loc p in
194
(sep() ++ if prec_less prec inh then strm else surround strm)
196
let pr_patt = pr_patt mt
198
let pr_eqn pr (loc,pl,rhs) =
199
let pl = List.map snd pl in
201
(pr_with_comments loc
203
hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl
205
pr_sep_com spc (pr ltop) rhs))
207
let begin_of_binder = function
208
LocalRawDef((loc,_),_) -> fst (unloc loc)
209
| LocalRawAssum((loc,_)::_,_,_) -> fst (unloc loc)
212
let begin_of_binders = function
213
| b::_ -> begin_of_binder b
216
let surround_impl k p =
218
| Explicit -> str"(" ++ p ++ str")"
219
| Implicit -> str"{" ++ p ++ str"}"
221
let surround_binder k p =
223
| Default b -> hov 1 (surround_impl b p)
224
| Generalized (b, b', t) ->
225
hov 1 (surround_impl b' (surround_impl b p))
227
let surround_implicit k p =
229
| Default Explicit -> p
230
| Default Implicit -> (str"{" ++ p ++ str"}")
231
| Generalized (b, b', t) ->
232
surround_impl b' (surround_impl b p)
234
let pr_binder many pr (nal,k,t) =
236
| CHole _ -> prlist_with_sep spc pr_lname nal
238
let s = prlist_with_sep spc pr_lname nal ++ str" : " ++ pr t in
239
hov 1 (if many then surround_binder k s else surround_implicit k s)
241
let pr_binder_among_many pr_c = function
242
| LocalRawAssum (nal,k,t) ->
243
pr_binder true pr_c (nal,k,t)
244
| LocalRawDef (na,c) ->
245
let c,topt = match c with
246
| CCast(_,c, CastConv (_,t)) -> c, t
247
| _ -> c, CHole (dummy_loc, None) in
248
hov 1 (pr_lname na ++ pr_opt_type pr_c topt ++
249
str":=" ++ cut() ++ pr_c c)
251
let pr_undelimited_binders pr_c =
252
prlist_with_sep spc (pr_binder_among_many pr_c)
254
let pr_delimited_binders kw pr_c bl =
255
let n = begin_of_binders bl in
257
| [LocalRawAssum (nal,k,t)] ->
258
pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t)
259
| LocalRawAssum _ :: _ as bdl ->
260
pr_com_at n ++ kw() ++ pr_undelimited_binders pr_c bdl
263
let rec extract_prod_binders = function
264
(* | CLetIn (loc,na,b,c) as x ->
265
let bl,c = extract_prod_binders c in
266
if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
267
| CProdN (loc,[],c) ->
268
extract_prod_binders c
269
| CProdN (loc,(nal,bk,t)::bl,c) ->
270
let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in
271
LocalRawAssum (nal,bk,t) :: bl, c
274
let rec extract_lam_binders = function
275
(* | CLetIn (loc,na,b,c) as x ->
276
let bl,c = extract_lam_binders c in
277
if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
278
| CLambdaN (loc,[],c) ->
279
extract_lam_binders c
280
| CLambdaN (loc,(nal,bk,t)::bl,c) ->
281
let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
282
LocalRawAssum (nal,bk,t) :: bl, c
285
let split_lambda = function
286
| CLambdaN (loc,[[na],bk,t],c) -> (na,t,c)
287
| CLambdaN (loc,([na],bk,t)::bl,c) -> (na,t,CLambdaN(loc,bl,c))
288
| CLambdaN (loc,(na::nal,bk,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,bk,t)::bl,c))
289
| _ -> anomaly "ill-formed fixpoint body"
291
let rename na na' t c =
293
| (_,Name id), (_,Name id') -> (na',t,replace_vars_constr_expr [id,id'] c)
294
| (_,Name id), (_,Anonymous) -> (na,t,c)
297
let split_product na' = function
298
| CArrow (loc,t,c) -> (na',t,c)
299
| CProdN (loc,[[na],bk,t],c) -> rename na na' t c
300
| CProdN (loc,([na],bk,t)::bl,c) -> rename na na' t (CProdN(loc,bl,c))
301
| CProdN (loc,(na::nal,bk,t)::bl,c) ->
302
rename na na' t (CProdN(loc,(nal,bk,t)::bl,c))
303
| _ -> anomaly "ill-formed fixpoint body"
305
let merge_binders (na1,bk1,ty1) cofun (na2,bk2,ty2) codom =
307
match snd na1, snd na2 with
308
Anonymous, Name id ->
309
if occur_var_constr_expr id cofun then
310
failwith "avoid capture"
312
| Name id, Anonymous ->
313
if occur_var_constr_expr id codom then
314
failwith "avoid capture"
316
| Anonymous, Anonymous -> na1
317
| Name id1, Name id2 ->
318
if id1 <> id2 then failwith "not same name" else na1 in
324
Constrextern.check_same_type ty1 ty2;
326
(LocalRawAssum ([na],bk1,ty), codom)
328
let rec strip_domain bvar cofun c =
331
merge_binders bvar cofun ((dummy_loc,Anonymous),default_binder_kind,a) b
332
| CProdN(loc,[([na],bk,ty)],c') ->
333
merge_binders bvar cofun (na,bk,ty) c'
334
| CProdN(loc,([na],bk,ty)::bl,c') ->
335
merge_binders bvar cofun (na,bk,ty) (CProdN(loc,bl,c'))
336
| CProdN(loc,(na::nal,bk,ty)::bl,c') ->
337
merge_binders bvar cofun (na,bk,ty) (CProdN(loc,(nal,bk,ty)::bl,c'))
338
| _ -> failwith "not a product"
340
(* Note: binder sharing is lost *)
341
let rec strip_domains (nal,bk,ty) cofun c =
345
let bnd, c' = strip_domain (na,bk,ty) cofun c in
348
let f = CLambdaN(dummy_loc,[(nal,bk,ty)],cofun) in
349
let bnd, c1 = strip_domain (na,bk,ty) f c in
351
let bl, rest, c2 = strip_domains (nal,bk,ty) cofun c1 in
353
with Failure _ -> ([bnd],Some (nal,bk,ty), c1))
355
(* Re-share binders *)
356
let rec factorize_binders = function
357
| ([] | [_] as l) -> l
358
| LocalRawAssum (nal,k,ty) as d :: (LocalRawAssum (nal',k',ty')::l as l') ->
360
let _ = Constrextern.check_same_type ty ty' in
361
factorize_binders (LocalRawAssum (nal@nal',k,ty)::l)
363
d :: factorize_binders l')
364
| d :: l -> d :: factorize_binders l
366
(* Extract lambdas when a type constraint occurs *)
367
let rec extract_def_binders c ty =
369
| CLambdaN(loc,bvar::lams,b) ->
371
let f = CLambdaN(loc,lams,b) in
372
let bvar', rest, ty' = strip_domains bvar f ty in
374
match rest, lams with
377
| Some bvar,_ -> CLambdaN(loc,bvar::lams,b) in
378
let (bl,c2,ty2) = extract_def_binders c' ty' in
379
(factorize_binders (bvar'@bl), c2, ty2)
384
let rec split_fix n typ def =
385
if n = 0 then ([],typ,def)
387
let (na,_,def) = split_lambda def in
388
let (na,t,typ) = split_product na typ in
389
let (bl,typ,def) = split_fix (n-1) typ def in
390
(LocalRawAssum ([na],default_binder_kind,t)::bl,typ,def)
392
let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
394
if dangling_with_for then pr_dangling else pr in
395
pr_id id ++ str" " ++
396
hov 0 (pr_undelimited_binders (pr ltop) bl ++ annot) ++
397
pr_opt_type_spc pr t ++ str " :=" ++
398
pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
400
let pr_fixdecl pr prd dangling_with_for ((_,id),(n,ro),bl,t,c) =
404
if List.length bl > 1 && n <> None then
405
spc() ++ str "{struct " ++ pr_id (snd (Option.get n)) ++ str"}"
408
spc () ++ str "{wf " ++ pr lsimple c ++ pr_id (snd (Option.get n)) ++ str"}"
410
spc () ++ str "{measure " ++ pr lsimple c ++ pr_id (snd (Option.get n)) ++ str"}"
412
pr_recursive_decl pr prd dangling_with_for id bl annot t c
414
let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) =
415
pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c
417
let pr_recursive pr_decl id = function
418
| [] -> anomaly "(co)fixpoint with no definition"
419
| [d1] -> pr_decl false d1
421
prlist_with_sep (fun () -> fnl() ++ str "with ")
423
fnl() ++ str "for " ++ pr_id id
425
let is_var id = function
426
| CRef (Ident (_,id')) when id=id' -> true
429
let tm_clash = function
430
| (CRef (Ident (_,id)), Some (CApp (_,_,nal)))
431
when List.exists (function CRef (Ident (_,id')),_ -> id=id' | _ -> false)
434
| (CRef (Ident (_,id)), Some (CAppExpl (_,_,nal)))
435
when List.exists (function CRef (Ident (_,id')) -> id=id' | _ -> false)
440
let pr_asin pr (na,indnalopt) =
441
(match na with (* Decision of printing "_" or not moved to constrextern.ml *)
442
| Some na -> spc () ++ str "as " ++ pr_name na
444
(match indnalopt with
446
| Some t -> spc () ++ str "in " ++ pr lsimple t)
448
let pr_case_item pr (tm,asin) =
449
hov 0 (pr (lcast,E) tm ++ pr_asin pr asin)
451
let pr_case_type pr po =
453
| None | Some (CHole _) -> mt()
455
spc() ++ hov 2 (str "return" ++ pr_sep_com spc (pr lsimple) p)
457
let pr_return_type pr po = pr_case_type pr po
459
let pr_simple_return_type pr na po =
462
spc () ++ str "as " ++ pr_id id
466
let pr_proj pr pr_app a f l =
467
hov 0 (pr lsimple a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")")
469
let pr_appexpl pr f l =
471
str "@" ++ pr_reference f ++
472
prlist (pr_sep_com spc (pr (lapp,L))) l)
477
prlist (fun a -> spc () ++ pr_expl_args pr a) l)
480
if !Flags.unicode_syntax then str"Π" ++ spc ()
481
else str"forall" ++ spc ()
484
if !Flags.unicode_syntax then str"λ" ++ spc ()
485
else str"fun" ++ spc ()
487
let pr_fun_sep = lazy (if !Flags.unicode_syntax then str "," else str " =>")
489
let rec pr sep inherited a =
490
let (strm,prec) = match a with
491
| CRef r -> pr_reference r, latom
495
(pr_fixdecl (pr mt) (pr_dangling_with_for mt)) (snd id) fix),
497
| CCoFix (_,id,cofix) ->
498
hov 0 (str "cofix " ++
500
(pr_cofixdecl (pr mt) (pr_dangling_with_for mt)) (snd id) cofix),
503
hov 0 (pr mt (larrow,L) a ++ str " ->" ++
504
pr (fun () ->brk(1,0)) (-larrow,E) b),
507
let (bl,a) = extract_prod_binders a in
509
hov 2 (pr_delimited_binders pr_forall
511
str "," ++ pr spc ltop a),
514
let (bl,a) = extract_lam_binders a in
516
hov 2 (pr_delimited_binders pr_fun
518
Lazy.force pr_fun_sep ++ pr spc ltop a),
520
| CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b)
523
hov 2 (str "let " ++ pr mt ltop fx ++ str " in") ++
526
| CLetIn (_,x,a,b) ->
528
hov 2 (str "let " ++ pr_lname x ++ str " :=" ++
529
pr spc ltop a ++ str " in") ++
532
| CAppExpl (_,(Some i,f),l) ->
533
let l1,l2 = list_chop i l in
534
let c,l1 = list_sep_last l1 in
535
let p = pr_proj (pr mt) pr_appexpl c f l1 in
537
p ++ prlist (pr spc (lapp,L)) l2, lapp
540
| CAppExpl (_,(None,Ident (_,var)),[t])
541
| CApp (_,(_,CRef(Ident(_,var))),[t,None])
542
when var = Topconstr.ldots_var ->
543
hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg
544
| CAppExpl (_,(None,f),l) -> pr_appexpl (pr mt) f l, lapp
545
| CApp (_,(Some i,f),l) ->
546
let l1,l2 = list_chop i l in
547
let c,l1 = list_sep_last l1 in
548
assert (snd c = None);
549
let p = pr_proj (pr mt) pr_app (fst c) f l1 in
551
p ++ prlist (fun a -> spc () ++ pr_expl_args (pr mt) a) l2, lapp
554
| CApp (_,(None,a),l) -> pr_app (pr mt) a l, lapp
559
| Some t -> spc () ++ pr spc ltop t ++ spc () ++ str"with" ++ spc ()
561
hv 0 (str"{" ++ beg ++
562
prlist_with_sep (fun () -> spc () ++ str";" ++ spc ())
563
(fun ((_,id), c) -> pr_id id ++ spc () ++ str":=" ++ spc () ++ pr spc ltop c)
566
| CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) ->
569
hov 0 (pr_patt ltop p ++
570
pr_asin (pr_dangling_with_for mt) asin ++
571
str " :=" ++ pr spc ltop c ++
572
pr_case_type (pr_dangling_with_for mt) rtntypopt ++
573
str " in" ++ pr spc ltop b)),
575
| CCases(_,_,rtntypopt,c,eqns) ->
577
(hv 0 (str "match" ++ brk (1,2) ++
579
prlist_with_sep sep_v
580
(pr_case_item (pr_dangling_with_for mt)) c
581
++ pr_case_type (pr_dangling_with_for mt) rtntypopt) ++
582
spc () ++ str "with") ++
583
prlist (pr_eqn (pr mt)) eqns ++ spc() ++ str "end"),
585
| CLetTuple (_,nal,(na,po),c,b) ->
589
prlist_with_sep sep_v pr_name nal ++
591
pr_simple_return_type (pr mt) na po ++ str " :=" ++
592
pr spc ltop c ++ str " in") ++
595
| CIf (_,c,(na,po),b1,b2) ->
596
(* On force les parenthèses autour d'un "if" sous-terme (même si le
597
parsing est lui plus tolérant) *)
599
hov 1 (str "if " ++ pr mt ltop c ++ pr_simple_return_type (pr mt) na po) ++
601
hov 0 (str "then" ++ pr (fun () -> brk (1,1)) ltop b1) ++ spc () ++
602
hov 0 (str "else" ++ pr (fun () -> brk (1,1)) ltop b2)),
605
| CHole _ -> str "_", latom
606
| CEvar (_,n,l) -> pr_evar (pr mt) n l, latom
607
| CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
608
| CSort (_,s) -> pr_rawsort s, latom
609
| CCast (_,a,CastConv (k,b)) ->
610
let s = match k with VMcast -> "<:" | DEFAULTcast -> ":" in
611
hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b),
613
| CCast (_,a,CastCoerce) ->
614
hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"),
616
| CNotation (_,"( _ )",([t],[])) ->
617
pr (fun()->str"(") (max_int,L) t ++ str")", latom
618
| CNotation (_,s,env) -> pr_notation (pr mt) s env
619
| CGeneralization (_,bk,ak,c) -> pr_generalization bk ak (pr mt lsimple c), latom
620
| CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p
621
| CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1
622
| CDynamic _ -> str "<dynamic>", latom
624
let loc = constr_loc a in
626
(sep() ++ if prec_less prec inherited then strm else surround strm)
628
and pr_dangling_with_for sep inherited a =
630
| (CFix (_,_,[_])|CCoFix(_,_,[_])) -> pr sep (latom,E) a
631
| _ -> pr sep inherited a
635
let rec strip_context n iscast t =
637
[], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t
639
| CLambdaN (loc,(nal,bk,t)::bll,c) ->
640
let n' = List.length nal in
642
let nal1,nal2 = list_chop n nal in
643
[LocalRawAssum (nal1,bk,t)], CLambdaN (loc,(nal2,bk,t)::bll,c)
645
let bl', c = strip_context (n-n') iscast
646
(if bll=[] then c else CLambdaN (loc,bll,c)) in
647
LocalRawAssum (nal,bk,t) :: bl', c
648
| CProdN (loc,(nal,bk,t)::bll,c) ->
649
let n' = List.length nal in
651
let nal1,nal2 = list_chop n nal in
652
[LocalRawAssum (nal1,bk,t)], CProdN (loc,(nal2,bk,t)::bll,c)
654
let bl', c = strip_context (n-n') iscast
655
(if bll=[] then c else CProdN (loc,bll,c)) in
656
LocalRawAssum (nal,bk,t) :: bl', c
657
| CArrow (loc,t,c) ->
658
let bl', c = strip_context (n-1) iscast c in
659
LocalRawAssum ([loc,Anonymous],default_binder_kind,t) :: bl', c
660
| CCast (_,c,_) -> strip_context n false c
661
| CLetIn (_,na,b,c) ->
662
let bl', c = strip_context (n-1) iscast c in
663
LocalRawDef (na,b) :: bl', c
664
| _ -> anomaly "strip_context"
667
pr_constr_expr : constr_expr -> std_ppcmds;
668
pr_lconstr_expr : constr_expr -> std_ppcmds;
669
pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds;
670
pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
673
let default_term_pr = {
674
pr_constr_expr = pr lsimple;
675
pr_lconstr_expr = pr ltop;
676
pr_constr_pattern_expr = pr lsimple;
677
pr_lconstr_pattern_expr = pr ltop
680
let term_pr = ref default_term_pr
682
let set_term_pr = (:=) term_pr
684
let pr_constr_expr c = !term_pr.pr_constr_expr c
685
let pr_lconstr_expr c = !term_pr.pr_lconstr_expr c
686
let pr_constr_pattern_expr c = !term_pr.pr_constr_pattern_expr c
687
let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c
689
let pr_cases_pattern_expr = pr_patt ltop
691
let pr_binders = pr_undelimited_binders (pr ltop)
693
let pr_with_occurrences_with_trailer pr occs trailer =
695
((false,[]),c) -> pr c ++ trailer
696
| ((nowhere_except_in,nl),c) ->
697
hov 1 (pr c ++ spc() ++ str"at " ++
698
(if nowhere_except_in then mt() else str "- ") ++
699
hov 0 (prlist_with_sep spc (pr_or_var int) nl) ++ trailer)
701
let pr_with_occurrences pr occs =
702
pr_with_occurrences_with_trailer pr occs (mt())
704
let pr_red_flag pr r =
705
(if r.rBeta then pr_arg str "beta" else mt ()) ++
706
(if r.rIota then pr_arg str "iota" else mt ()) ++
707
(if r.rZeta then pr_arg str "zeta" else mt ()) ++
708
(if r.rConst = [] then
709
if r.rDelta then pr_arg str "delta"
712
pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
713
hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
717
let pr_metaid id = str"?" ++ pr_id id
719
let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
720
| Red false -> str "red"
722
| Simpl o -> str "simpl" ++ pr_opt (pr_with_occurrences pr_constr) o
724
if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then
727
hov 1 (str "cbv" ++ pr_red_flag pr_ref f)
729
hov 1 (str "lazy" ++ pr_red_flag pr_ref f)
731
hov 1 (str "unfold" ++ spc() ++
732
prlist_with_sep pr_coma (pr_with_occurrences pr_ref) l)
733
| Fold l -> hov 1 (str "fold" ++ prlist (pr_arg pr_constr) l)
735
hov 1 (str "pattern" ++
736
pr_arg (prlist_with_sep pr_coma (pr_with_occurrences pr_constr)) l)
738
| Red true -> error "Shouldn't be accessible from user."
739
| ExtraRedExpr s -> str s
740
| CbvVm -> str "vm_compute"
742
let rec pr_may_eval test prc prlc pr2 = function
743
| ConstrEval (r,c) ->
745
(str "eval" ++ brk (1,1) ++
746
pr_red_expr (prc,prlc,pr2) r ++
747
str " in" ++ spc() ++ prc c)
748
| ConstrContext ((_,id),c) ->
750
(str "context " ++ pr_id id ++ spc () ++
751
str "[" ++ prlc c ++ str "]")
752
| ConstrTypeOf c -> hov 1 (str "type of" ++ spc() ++ prc c)
753
| ConstrTerm c when test c -> h 0 (str "(" ++ prc c ++ str ")")
754
| ConstrTerm c -> prc c
756
let pr_may_eval a = pr_may_eval (fun _ -> false) a
added
removed
parsing/ppconstr.ml
