helm/software/components/tptp_grafite/mainTHF.ml

   1 module T = CicNotationPt
   2 module GA = GrafiteAst
   3 module A = AstTHF
   4
   5 let floc = HExtlib.dummy_floc;;
   6
   7 (* OPTIONS *)
   8 let tptppath = ref "./";;
   9 let ng = ref false;;
  10 let spec = [
  11   ("-ng",Arg.Set ng,"Matita ng syntax");
  12   ("-tptppath",
  13       Arg.String (fun x -> tptppath := x),
  14       "Where to find the Axioms/ and Problems/ directory")
  15 ]
  16
  17 let resolve ~tptppath s =
  18   if s.[0] = '/' then s else
  19   let resolved_name =
  20     if Filename.check_suffix s ".p" then
  21       (assert (String.length s > 5);
  22       let prefix = String.sub s 0 3 in
  23       tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
  24     else
  25       tptppath ^ "/" ^ s
  26   in
  27   if HExtlib.is_regular resolved_name then
  28     resolved_name
  29   else
  30     begin
  31       prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
  32       exit 1
  33     end
  34 ;;
  35
  36
  37 let find_related id =
  38   HExtlib.filter_map_monad
  39     (fun acc -> function
  40       | A.ThfDefinition (_,did,dbody) when did = id -> Some dbody, None
  41       | A.ThfType (_,did,dtype) when did = id -> Some dtype, None
  42       | x -> acc, Some x)
  43 ;;
  44
  45 (* MAIN *)
  46 let _ =
  47   let usage = "Usage: tptpTHF2grafite [options] file" in
  48   let inputfile = ref "" in
  49   Arg.parse spec (fun s -> inputfile := s) usage;
  50   if !inputfile = "" then
  51     begin
  52       prerr_endline usage;
  53       exit 1
  54     end;
  55   let tptppath = !tptppath in
  56   let statements =
  57     let rec aux = function
  58       | [] -> []
  59       | ((A.Inclusion (file,_)) as hd) :: tl ->
  60           let file = resolve ~tptppath file in
  61           let lexbuf = Lexing.from_channel (open_in file) in
  62           let statements = ParserTHF.main LexerTHF.yylex lexbuf in
  63           hd :: aux (statements @ tl)
  64       | hd::tl -> hd :: aux tl
  65     in
  66      aux [A.Inclusion (!inputfile,[])]
  67   in
  68   let statements =
  69     let rec aux = function
  70       | [] -> []
  71       | A.Comment s :: tl ->
  72          let s = Pcre.replace ~pat:"\n" ~templ:"" s in
  73          let s = Pcre.replace ~pat:"\\*\\)" ~templ:"" s in
  74          GA.Comment (floc,GA.Note (floc,s)) :: aux tl
  75       | A.Inclusion (s,_) :: tl ->
  76         GA.Comment (
  77           floc, GA.Note (
  78             floc,"Inclusion of: " ^ s)) :: aux tl
  79       | A.ThfType(name,id,ty) :: tl ->
  80          let body, tl = find_related id None tl in
  81          let what = match body with None -> `Axiom | _ -> `Definition in
  82          GA.Executable(floc,
  83           GA.NCommand(floc,
  84            GA.NObj(floc,
  85             T.Theorem(what, id,ty,body,`Regular)))) :: aux tl
  86       | A.ThfDefinition(name,id,body) :: tl ->
  87          let ty, tl = find_related id None tl in
  88          let ty = match ty with Some x -> x | None -> T.Implicit `JustOne in
  89          GA.Executable(floc,
  90           GA.NCommand(floc,
  91            GA.NObj(floc,
  92             T.Theorem(`Definition,
  93              id,ty,Some body,`Regular)))):: aux tl
  94       | A.ThfFormula(name,(A.Axiom|A.Hypothesis|A.Assumption),term) :: tl ->
  95          GA.Executable(floc,
  96           GA.NCommand(floc,
  97            GA.NObj(floc,
  98             T.Theorem(`Axiom, name,term,None,`Regular)))):: aux tl
  99       | A.ThfFormula(name,A.Conjecture,term) :: tl ->
 100          GA.Executable(floc,
 101           GA.NCommand(floc,
 102            GA.NObj(floc,
 103             T.Theorem(`Theorem, name,
 104              term,None,`Regular)))):: aux tl
 105       | A.ThfFormula _ :: tl -> assert false
 106     in
 107       aux statements
 108   in
 109   let pp t =
 110     (* ZACK: setting width to 80 will trigger a bug of BoxPp.render_to_string
 111      * which will show up using the following command line:
 112      * ./tptp2grafite -tptppath ~tassi/TPTP-v3.1.1 GRP170-1 *)
 113     let width = max_int in
 114     let term_pp prec content_term =
 115       let pres_term = TermContentPres.pp_ast content_term in
 116       let lookup_uri = fun _ -> None in
 117       let markup = CicNotationPres.render ~lookup_uri ~prec pres_term in
 118       let s = BoxPp.render_to_string List.hd width markup ~map_unicode_to_tex:false in
 119       Pcre.substitute
 120        ~rex:(Pcre.regexp ~flags:[`UTF8] "∀[Ha-z][a-z0-9_]*") ~subst:(fun x -> "\n" ^ x)
 121        s
 122     in
 123     CicNotationPp.set_pp_term (term_pp 90);
 124     let lazy_term_pp = fun x -> assert false in
 125     let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
 126     Pcre.replace ~pat:"^theorem" ~templ:"ntheorem"
 127     (Pcre.replace ~pat:"^axiom" ~templ:"naxiom"
 128     (Pcre.replace ~pat:"^definition" ~templ:"ndefinition"
 129     (Pcre.replace ~pat:"Type \\\\sub ([0-9]+)" ~templ:"Type[$1]"
 130      (GrafiteAstPp.pp_statement
 131        ~map_unicode_to_tex:false
 132          ~term_pp:(term_pp 19) ~lazy_term_pp ~obj_pp t))))
 133   in
 134   print_endline (pp (GA.Executable (floc,
 135     GA.Command(floc,GA.Include(floc,true,`OldAndNew,"TPTP.ma")))));
 136   List.iter (fun x -> print_endline (pp x)) statements;
 137   exit 0
 138