2 ref (fun ~context ~subst ~metasenv ?inside_fix t -> "Please, set a pp callback")
5 let set_ppterm f = ppterm := f;;
7 let ppterm ~context ~subst ~metasenv ?inside_fix t =
8 !ppterm ~context ~subst ~metasenv ?inside_fix t
14 let r2s pp_fix_name r =
17 | R.Ref (_,u,R.Ind i) ->
18 (match snd(NCicEnvironment.get_obj u) with
19 | _,_,_,_, C.Inductive (_,_,itl,_) ->
20 let _,name,_,_ = List.nth itl i in name
22 | R.Ref (_,u,R.Con (i,j)) ->
23 (match snd(NCicEnvironment.get_obj u) with
24 | _,_,_,_, C.Inductive (_,_,itl,_) ->
25 let _,_,_,cl = List.nth itl i in
26 let _,name,_ = List.nth cl (j-1) in name
28 | R.Ref (_,u,(R.Decl | R.Def )) ->
29 (match snd(NCicEnvironment.get_obj u) with
30 | _,_,_,_, C.Constant (_,name,_,_,_) -> name
32 | R.Ref (_,u,(R.Fix (i,_)|R.CoFix i)) ->
33 (match snd(NCicEnvironment.get_obj u) with
34 | _,_,_,_, C.Fixpoint (_,fl,_) ->
36 let _,name,_,_,_ = List.nth fl i in name
38 let name = NUri.string_of_uri u in
39 let name = Filename.basename name in
40 let name = Filename.chop_extension name in
41 name ^"("^ string_of_int i ^ ")"
43 with exn -> R.string_of_reference r
46 let trivial_pp_term ~context ~subst ~metasenv ?(inside_fix=false) t =
47 let buff = Buffer.create 100 in
48 let f = Format.formatter_of_buffer buff in
49 let module F = Format in
50 let rec aux ctx = function
52 (try F.fprintf f "%s" (List.nth ctx (m-1))
53 with Failure _ -> F.fprintf f " -%d" (m - List.length context))
54 | C.Const r -> F.fprintf f "%s" (r2s inside_fix r)
56 F.fprintf f "@[<hov 1>";
61 | C.Prod (name,s,t) ->
62 F.fprintf f "@[<hov 1>";
63 F.fprintf f "@[<hov 2>∀%s:@;" name;
68 | C.Lambda (name,s,t) ->
69 F.fprintf f "@[<hov 1>";
70 F.fprintf f "λ%s:" name;
75 | C.LetIn (name,ty,t,b) ->
76 F.fprintf f "let %s:" name;
82 | C.Match (r,oty,t,pl) ->
83 F.fprintf f "@[<hov>match ";
85 F.fprintf f "@;return ";
87 F.fprintf f "@; @[<v>[ ";
90 F.fprintf f "@[<hov 2>%s ⇒@;" (r2s inside_fix (R.mk_constructor 1 r));
95 F.fprintf f "@;| @[<hov 2>%s ⇒@;" (r2s inside_fix (R.mk_constructor i r));
101 F.fprintf f "]@] @]";
103 F.fprintf f "@[<h 2>(";
105 List.iter (fun x -> F.fprintf f "@;";aux ctx x) (List.tl l);
107 | C.Implicit _ -> F.fprintf f "?"
108 | C.Meta (n,_) -> F.fprintf f "?%d" n
109 | C.Sort C.Prop -> F.fprintf f "Prop"
110 | C.Sort C.CProp -> F.fprintf f "CProp"
111 | C.Sort (C.Type n) -> F.fprintf f "Type%d" n
113 aux (List.map fst context) t;
119 | (u,_,metasenv,subst,NCic.Fixpoint (b, fl, _)) ->
120 "{"^NUri.string_of_uri u^"}\n"^
122 String.concat "\nand " (fst
123 (List.fold_right (fun (_,name,n,ty,bo) (l,i) ->
125 " on " ^ string_of_int n ^ " : " ^
126 ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^
127 ppterm ~metasenv ~subst ~context:[] ~inside_fix:true bo) :: l),i-1) fl
128 ([],List.length fl)))
129 | (u,_,_,_,NCic.Inductive (b, _,tyl, _)) -> "inductive"
130 | (u,_,metasenv,subst,NCic.Constant (_,name,None,ty, _)) ->
131 "axiom " ^ name ^ " : " ^
132 ppterm ~metasenv ~subst ~context:[] ty ^ "\n"
133 | (u,_,metasenv,subst,NCic.Constant (_,name,Some bo,ty, _)) ->
134 "definition " ^ name ^ " : " ^
135 ppterm ~metasenv ~subst ~context:[] ty ^ " := \n"^
136 ppterm ~metasenv ~subst ~context:[] bo ^ "\n"