+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.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
let parse_error s = Printf.eprintf "%s: " s ;;
let rm_q s = String.sub s 1 (String.length s - 2) ;;
+
+let reserved = [
+ "in","In";
+ "to","To";
+ "theorem","Theorem";
+];;
+
+let unreserve k =
+ try List.assoc k reserved with Not_found -> k
+;;
+
%}
%token <string> TYPE
;
annot_formula:
- | THF LPAREN
- name COMMA formula_type COMMA term formula_source_and_infos
- RPAREN DOT {
- Formula($3,$5,$7)
+ | THF LPAREN name COMMA formula_type COMMA
+ term formula_source_and_infos RPAREN DOT {
+ match $5 with
+ | Definition ->
+ (match $7 with
+ | T.Appl [T.Symbol("Eq",_);T.Ident(name,_);body] ->
+ ThfDefinition($3,unreserve name,body)
+ | _ -> prerr_endline ("near " ^ $3); assert false)
+ | Type ->
+ (match $7 with
+ | T.Cast (T.Ident(name,_),ty) -> ThfType($3,unreserve name,ty)
+ | _ -> assert false)
+ | _ -> ThfFormula($3,$5,$7)
}
;
| LAMBDA {`Lambda}
vardecl :
- | UNAME { T.Implicit `JustOne,Some (T.Ident($1,None)) }
- | UNAME COLON term { $3,Some (T.Ident($1,None)) }
+ | UNAME { T.Ident($1,None), None }
+ | UNAME COLON term { T.Ident($1,None),Some $3 }
varlist :
| vardecl { [$1] }
| quantifier BEGINVARLIST varlist ENDVARLIST COLON term {
List.fold_right (fun v t -> T.Binder($1,v,t)) $3 $6
}
- | term IMPLY term {
- match $1 with
- | T.Appl l -> T.Appl (l @ [$3])
- | x -> T.Appl ([$1; $3])
- }
| term APPLY term {
match $1 with
| T.Appl l -> T.Appl (l @ [$3])
| x -> T.Appl ([$1; $3])
}
| LPAREN term COLON term RPAREN { T.Cast ($2,$4) }
- | term TO term { T.Binder (`Pi,($1,None),$3) }
- | term IEQ term { T.Appl [T.Symbol("'eq",0);$1;$3] }
- | term IAND term { T.Appl [T.Symbol("'and",0);$1;$3] }
- | term IOR term { T.Appl [T.Symbol("'or",0);$1;$3] }
- | NOT term { T.Appl [T.Symbol("'not",0);$2] }
+ | term TO term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
+ | term IMPLY term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
+ | term IEQ term { T.Appl [T.Symbol("Eq",0);$1;$3] }
+ | term IAND term { T.Appl [T.Symbol("And",0);$1;$3] }
+ | term IOR term { T.Appl [T.Symbol("Or",0);$1;$3] }
+ | NOT term { T.Appl [T.Symbol("Not",0);$2] }
| LPAREN term RPAREN {$2}
- | LNAME { T.Ident($1,None) }
+ | LNAME { T.Ident(unreserve $1,None) }
| UNAME { T.Ident($1,None) }
- | TYPE_I { T.Symbol("'i",0) }
- | TYPE_O { T.Symbol("'o",0) }
- | TYPE_U { T.Sort `Set }
- | FALSE { T.Symbol("'false",0)}
- | TRUE { T.Symbol("'true",0)}
+ | TYPE_I { T.Symbol("i",0) }
+ | TYPE_O { T.Symbol("o",0) }
+ | TYPE_U { T.Sort (`NType "0") }
+ | FALSE { T.Symbol("False",0)}
+ | TRUE { T.Symbol("True",0)}
;
include_:
projects / helm.git / commitdiff