+module T = CicNotationPt
+module GA = GrafiteAst
+module A = AstTHF
+
+let floc = HExtlib.dummy_floc;;
+
(* OPTIONS *)
let tptppath = ref "./";;
let ng = ref false;;
"Where to find the Axioms/ and Problems/ directory")
]
+let resolve ~tptppath s =
+ if s.[0] = '/' then s else
+ let resolved_name =
+ if Filename.check_suffix s ".p" then
+ (assert (String.length s > 5);
+ let prefix = String.sub s 0 3 in
+ tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
+ else
+ tptppath ^ "/" ^ s
+ in
+ if HExtlib.is_regular resolved_name then
+ resolved_name
+ else
+ begin
+ prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
+ exit 1
+ end
+;;
+
+
+let find_related id =
+ HExtlib.filter_map_monad
+ (fun acc -> function
+ | A.ThfDefinition (_,did,dbody) when did = id -> Some dbody, None
+ | A.ThfType (_,did,dtype) when did = id -> Some dtype, None
+ | x -> acc, Some x)
+;;
+
(* MAIN *)
let _ =
let usage = "Usage: tptpTHF2grafite [options] file" in
prerr_endline usage;
exit 1
end;
- let lexbuf = Lexing.from_channel (open_in !inputfile) in
- List.iter
- (function
- | AstTHF.Comment _ -> ()
- | AstTHF.Inclusion _ -> ()
- | AstTHF.Formula(name,role,term) ->
- prerr_endline (name ^ "===" ^ CicNotationPp.pp_term term)
-
- )
- (ParserTHF.main LexerTHF.yylex lexbuf);
+ 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;
exit 0