F.fprintf f "@; @[<v>[ ";
if pl <> [] then
begin
- F.fprintf f "@[<hov 2>%s ⇒@;" (r2s inside_fix (R.mk_constructor 1 r));
+ F.fprintf f "@[<hov 2>%s ⇒@;"
+ (try r2s inside_fix (R.mk_constructor 1 r)
+ with R.IllFormedReference _ -> "#ERROR#");
aux ~toplevel:true ctx (List.hd pl);
F.fprintf f "@]";
ignore(List.fold_left
(fun i t ->
- F.fprintf f "@;| @[<hov 2>%s ⇒@;" (r2s inside_fix (R.mk_constructor i r));
+ F.fprintf f "@;| @[<hov 2>%s ⇒@;"
+ (try r2s inside_fix (R.mk_constructor i r)
+ with R.IllFormedReference _ -> "#ERROR#");
aux ~toplevel:true ctx t;
F.fprintf f "@]";
i+1)
2 (List.tl pl));
end;
F.fprintf f "]@] @]";
+ | C.Appl [] | C.Appl [_] | C.Appl (C.Appl _::_) ->
+ F.fprintf f "BAD APPLICATION"
| C.Appl l ->
F.fprintf f "@[<hov 2>";
if not toplevel then F.fprintf f "(";
Buffer.contents buff
;;
-let ppobj = function
- | (u,_,metasenv,subst,NCic.Fixpoint (b, fl, _)) ->
- "{"^NUri.string_of_uri u^"}\n"^
- (if b then "let rec " else "let corec ") ^
- String.concat "\nand "
- (List.map (fun (_,name,n,ty,bo) ->
- name^ " on " ^ string_of_int n ^ " : " ^
- ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^
- ppterm ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl)
- | (u,_,metasenv,subst,NCic.Inductive (b, leftno,tyl, _)) ->
- "{"^NUri.string_of_uri u^"} with "^string_of_int leftno^" fixed params\n"^
- (if b then "inductive " else "coinductive ")^
- String.concat "\nand "
- (List.map (fun (_,name,ty,cl) ->
- name^": "^ppterm ~metasenv ~subst ~context:[] ty^ " :=\n"^
- String.concat "\n"
- (List.map (fun (_,name,ty) ->
- " | "^name^": "^ppterm ~metasenv ~subst ~context:[] ty)
- cl)) tyl) ^ "."
- | (u,_,metasenv,subst,NCic.Constant (_,name,None,ty, _)) ->
- "{"^NUri.string_of_uri u^"}\n"^
- "axiom " ^ name ^ " : " ^
- ppterm ~metasenv ~subst ~context:[] ty ^ "\n"
- | (u,_,metasenv,subst,NCic.Constant (_,name,Some bo,ty, _)) ->
- "{"^NUri.string_of_uri u^"}\n"^
- "definition " ^ name ^ " : " ^
- ppterm ~metasenv ~subst ~context:[] ty ^ " := \n"^
- ppterm ~metasenv ~subst ~context:[] bo ^ "\n"
+let ppterm ~context ~subst ~metasenv ?(margin=80) ?inside_fix t =
+ Format.set_margin margin;
+ ppterm ~context ~subst ~metasenv ?inside_fix t
;;
let rec ppcontext ?(sep="\n") ~subst ~metasenv = function
let rec ppmetasenv ~subst metasenv = function
| [] -> ""
| (i,(name, ctx, ty)) :: tl ->
- let name = match name with Some n -> "(\""^n^"\")" | _ -> "" in
+ let name = match name with Some n -> "("^n^")" | _ -> "" in
ppcontext ~sep:"; " ~subst ~metasenv ctx ^
" ⊢ ?"^string_of_int i^name^" : " ^
ppterm ~metasenv ~subst ~context:ctx ty ^ "\n" ^
let ppsubst ~metasenv subst = ppsubst ~metasenv ~subst subst;;
-let _ = NCicSubstitution.set_ppterm ppterm;;
+
+let ppobj (u,_,metasenv, subst, o) =
+ "metasenv:\n" ^ ppmetasenv ~subst metasenv ^ "\n" ^
+ "subst:\n" ^ ppsubst subst ~metasenv ^ "\n" ^
+ match o with
+ | NCic.Fixpoint (b, fl, _) ->
+ "{"^NUri.string_of_uri u^"}\n"^
+ (if b then "let rec " else "let corec ") ^
+ String.concat "\nand "
+ (List.map (fun (_,name,n,ty,bo) ->
+ name^ " on " ^ string_of_int n ^ " : " ^
+ ppterm ~metasenv ~subst ~context:[] ty ^ " :=\n"^
+ ppterm ~metasenv ~subst ~context:[] ~inside_fix:true bo) fl)
+ | NCic.Inductive (b, leftno,tyl, _) ->
+ "{"^NUri.string_of_uri u^"} with "^string_of_int leftno^" fixed params\n"^
+ (if b then "inductive " else "coinductive ")^
+ String.concat "\nand "
+ (List.map (fun (_,name,ty,cl) ->
+ name^": "^ppterm ~metasenv ~subst ~context:[] ty^ " :=\n"^
+ String.concat "\n"
+ (List.map (fun (_,name,ty) ->
+ " | "^name^": "^ppterm ~metasenv ~subst ~context:[] ty)
+ cl)) tyl) ^ "."
+ | NCic.Constant (_,name,None,ty, _) ->
+ "{"^NUri.string_of_uri u^"}\n"^
+ "axiom " ^ name ^ " : " ^
+ ppterm ~metasenv ~subst ~context:[] ty ^ "\n"
+ | NCic.Constant (_,name,Some bo,ty, _) ->
+ "{"^NUri.string_of_uri u^"}\n"^
+ "definition " ^ name ^ " : " ^
+ ppterm ~metasenv ~subst ~context:[] ty ^ " := \n"^
+ ppterm ~metasenv ~subst ~context:[] bo ^ "\n"
+;;
+
+let _ = NCicSubstitution.set_ppterm (ppterm ~margin:80);;