From: Enrico Tassi Date: Thu, 8 Apr 2010 14:43:43 +0000 (+0000) Subject: THF parser received some care X-Git-Tag: make_still_working~2941 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f3c3059ab94266de1cdf7cbd1bbc62231d2f9a22;p=helm.git THF parser received some care From: tassi --- diff --git a/helm/software/components/tptp_grafite/astTHF.ml b/helm/software/components/tptp_grafite/astTHF.ml index 541cf98e1..e47c69e65 100644 --- a/helm/software/components/tptp_grafite/astTHF.ml +++ b/helm/software/components/tptp_grafite/astTHF.ml @@ -17,6 +17,8 @@ type role = type ast = - | Formula of string * role * CicNotationPt.term + | ThfFormula of string * role * CicNotationPt.term + | ThfDefinition of string * string * CicNotationPt.term + | ThfType of string * string * CicNotationPt.term | Comment of string | Inclusion of string * (string list) diff --git a/helm/software/components/tptp_grafite/mainTHF.ml b/helm/software/components/tptp_grafite/mainTHF.ml index b3eca0141..ece02f4a0 100644 --- a/helm/software/components/tptp_grafite/mainTHF.ml +++ b/helm/software/components/tptp_grafite/mainTHF.ml @@ -1,3 +1,9 @@ +module T = CicNotationPt +module GA = GrafiteAst +module A = AstTHF + +let floc = HExtlib.dummy_floc;; + (* OPTIONS *) let tptppath = ref "./";; let ng = ref false;; @@ -8,6 +14,34 @@ let spec = [ "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 @@ -18,15 +52,87 @@ let _ = 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 diff --git a/helm/software/components/tptp_grafite/parserTHF.mly b/helm/software/components/tptp_grafite/parserTHF.mly index 35bc870cc..195b79f8d 100644 --- a/helm/software/components/tptp_grafite/parserTHF.mly +++ b/helm/software/components/tptp_grafite/parserTHF.mly @@ -7,6 +7,17 @@ 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 TYPE @@ -78,10 +89,19 @@ ; 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) } ; @@ -109,8 +129,8 @@ | 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] } @@ -120,30 +140,26 @@ | 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_: