Cross Reference: /hets/HolLight/OcamlTools/exportTools/export

Lines Matching defs:fmt
46 let pp_int fmt i = Format.fprintf fmt "%i" i
48 let pp_str fmt s = Format.fprintf fmt "%s" (xml_escape_str s)
50 let pp_inner_indented s e pi fmt i = Format.fprintf fmt "@[<hv>@[<hv 1>%s@,%a@]@,@]%s" s pi i e
52 let pp_inner_tuple p1 p2 fmt (_1,_2) = Format.fprintf fmt "%a@,%a" (pp_inner_indented "<fst>" "</fst>" p1) _1 (pp_inner_indented "<snd>" "</snd>" p2) _2
53 let pp_tuple p1 p2 fmt t = pp_inner_indented "<tuple>" "</tuple>" (pp_inner_tuple p1 p2) fmt t
55 let pp_parse_type fmt s =
56   if is_prefix s then Format.fprintf fmt "<Prefix />"
59                 (i,"right") -> Format.fprintf fmt "<InfixR>%u</InfixR>" i
60               | (i,"left") -> Format.fprintf fmt "<InfixL>%u</InfixL>" i
61               | _ -> Format.fprintf fmt "<Normal />"
62   else if parses_as_binder s then Format.fprintf fmt "<Binder />"
63   else Format.fprintf fmt "<Normal />"
65 let pp_term_info fmt (s0,ty0) = try let s = fst(find (fun (s,(s',ty)) -> s' = s0 & can (type_match ty ty0) []) (!the_interface))
66                                  in Format.fprintf fmt "@[<v>%a@,%a@]" pp_parse_type s0 (pp_tuple pp_str pp_parse_type) (s,s)
67                              with Failure _ -> Format.fprintf fmt "@[<h>%a@]" pp_parse_type s0
69 let rec pp_list pp_el fmt = function
70  | [h]  -> Format.fprintf fmt "%a" pp_el h
71  | h::t -> Format.fprintf fmt "%a@,%a" pp_el h (pp_list pp_el) t
74 let rec pp_shared_hol_type fmt = function
75  | Styvar s      -> pp_inner_indented "<TyVar>" "</TyVar>" pp_int fmt s
76  | Styapp (s,ts) -> pp_inner_indented "<TyApp>" "</TyApp>" (pp_tuple pp_int (pp_list (pp_inner_indented "<i>" "</i>" pp_int))) fmt (s,ts)
78 let rec pp_shared_term fmt = function
79  | Svar (s,h,t)    -> pp_inner_indented "<Var>" "</Var>" (fun fmt (s,h,t) -> Format.fprintf fmt "%a@,%a" (pp_tuple pp_int pp_int) (s,h) pp_term_info t) fmt (s,h,t)
80  | Sconst (s,h,t)  -> pp_inner_indented "<Const>" "</Const>" (fun fmt (s,h,t) -> Format.fprintf fmt "%a@,%a" (pp_tuple pp_int pp_int) (s,h) pp_term_info t) fmt (s,h,t)
81  | Scomb (t1,t2) -> pp_inner_indented "<Comb>" "</Comb>" (fun fmt (t1,t2) -> Format.fprintf fmt "%a" (pp_tuple pp_int pp_int) (t1,t2)) fmt (t1,t2)
82  | Sabs (t1,t2)  -> pp_inner_indented "<Abs>" "</Abs>" (fun fmt (t1,t2) -> Format.fprintf fmt "%a" (pp_tuple pp_int pp_int) (t1,t2)) fmt (t1,t2)
90 let pp_shared_hol_type_snd fmt d = pp_shared_hol_type fmt (snd d) 
91 let pp_shared_term_snd fmt d = pp_shared_term fmt (snd d)
93 let pp_hol_strings fmt d = pp_inner_indented "<Strings>" "</Strings>" (pp_list (pp_inner_indented "<s>" "</s>" pp_str)) fmt (map_snd (sharedtbl_to_list d))
94 let pp_shared_hol_types fmt d = pp_inner_indented "<SharedHolTypes>" "</SharedHolTypes>" (pp_list pp_shared_hol_type_snd) fmt (sharedtbl_to_list d)
95 let pp_shared_hol_terms fmt d = pp_inner_indented "<SharedHolTerms>" "</SharedHolTerms>" (pp_list pp_shared_term_snd) fmt (sharedtbl_to_list d)
99 let pp_export fmt (k,l) = pp_inner_indented "<HolExport>" "</HolExport>" (fun fmt (k,l) -> Format.fprintf fmt "%a@,%a@,%a@,%a@,%a" pp_hol_strings hol_strings pp_shared_hol_types shared_hol_types pp_shared_hol_terms shared_hol_terms pp_libs k pp_liblinks l) fmt (k,l)
103  let fmt = Format.formatter_of_out_channel out_ch in
104  printer fmt obj;