+ let tptppath = !tptppath in
+ let statements =
+ let rec aux = function
+ | [] -> []
+ | ((A.Inclusion (file,_)) as hd) :: tl ->
+ let file = resolve ~tptppath file in
+ let lexbuf = Lexing.from_channel (open_in file) in
+ let statements = ParserTHF.main LexerTHF.yylex lexbuf in
+ hd :: aux (statements @ tl)
+ | hd::tl -> hd :: aux tl
+ in
+ aux [A.Inclusion (!inputfile,[])]
+ in
+ let statements =
+ let rec aux = function
+ | [] -> []
+ | A.Comment s :: tl ->
+ let s = Pcre.replace ~pat:"\n" ~templ:"" s in
+ let s = Pcre.replace ~pat:"\\*\\)" ~templ:"" s in
+ GA.Comment (floc,GA.Note (floc,s)) :: aux tl
+ | A.Inclusion (s,_) :: tl ->
+ GA.Comment (
+ floc, GA.Note (
+ floc,"Inclusion of: " ^ s)) :: aux tl
+ | A.ThfType(name,id,ty) :: tl ->
+ let body, tl = find_related id None tl in
+ let what = match body with None -> `Axiom | _ -> `Definition in
+ GA.Executable(floc,
+ GA.NCommand(floc,
+ GA.NObj(floc,
+ T.Theorem(what, id,ty,body,`Regular)))) :: aux tl
+ | A.ThfDefinition(name,id,body) :: tl ->
+ let ty, tl = find_related id None tl in
+ let ty = match ty with Some x -> x | None -> T.Implicit `JustOne in
+ GA.Executable(floc,
+ GA.NCommand(floc,
+ GA.NObj(floc,
+ T.Theorem(`Definition,
+ id,ty,Some body,`Regular)))):: aux tl
+ | A.ThfFormula(name,(A.Axiom|A.Hypothesis|A.Assumption),term) :: tl ->
+ GA.Executable(floc,
+ GA.NCommand(floc,
+ GA.NObj(floc,
+ T.Theorem(`Axiom, name,term,None,`Regular)))):: aux tl
+ | A.ThfFormula(name,A.Conjecture,term) :: tl ->
+ GA.Executable(floc,
+ GA.NCommand(floc,
+ GA.NObj(floc,
+ T.Theorem(`Theorem, name,
+ term,None,`Regular)))):: aux tl
+ | A.ThfFormula _ :: tl -> assert false
+ in
+ aux statements
+ in
+ let pp t =
+ (* ZACK: setting width to 80 will trigger a bug of BoxPp.render_to_string
+ * which will show up using the following command line:
+ * ./tptp2grafite -tptppath ~tassi/TPTP-v3.1.1 GRP170-1 *)
+ let width = max_int in
+ let term_pp prec content_term =
+ let pres_term = TermContentPres.pp_ast content_term in
+ let lookup_uri = fun _ -> None in
+ let markup = CicNotationPres.render ~lookup_uri ~prec pres_term in
+ let s = BoxPp.render_to_string List.hd width markup ~map_unicode_to_tex:false in
+ Pcre.substitute
+ ~rex:(Pcre.regexp ~flags:[`UTF8] "∀[Ha-z][a-z0-9_]*") ~subst:(fun x -> "\n" ^ x)
+ s
+ in
+ CicNotationPp.set_pp_term (term_pp 90);
+ let lazy_term_pp = fun x -> assert false in
+ let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
+ Pcre.replace ~pat:"^theorem" ~templ:"ntheorem"
+ (Pcre.replace ~pat:"^axiom" ~templ:"naxiom"
+ (Pcre.replace ~pat:"^definition" ~templ:"ndefinition"
+ (Pcre.replace ~pat:"Type \\\\sub ([0-9]+)" ~templ:"Type[$1]"
+ (GrafiteAstPp.pp_statement
+ ~map_unicode_to_tex:false
+ ~term_pp:(term_pp 19) ~lazy_term_pp ~obj_pp t))))
+ in
+ print_endline (pp (GA.Executable (floc,
+ GA.Command(floc,GA.Include(floc,true,`OldAndNew,"TPTP.ma")))));
+ List.iter (fun x -> print_endline (pp x)) statements;