components/binaries/tptp2grafite/main.ml

   1 module GA = GrafiteAst;;
   2 module LA = LexiconAst;;
   3 module PT = CicNotationPt;;
   4 module A = Ast;;
   5 let floc = HExtlib.dummy_floc;;
   6
   7 let kw = [
   8  "and","myand"
   9 ];;
  10
  11 let mk_ident s =
  12   PT.Ident ((try List.assoc s kw with Not_found -> s),None)
  13 ;;
  14
  15
  16 let rec collect_arities_from_term = function
  17   | A.Constant name -> [name,0]
  18   | A.Variable name -> []
  19   | A.Function (name,l) ->
  20       (name,List.length l) :: List.flatten (List.map collect_arities_from_term l)
  21 ;;
  22
  23 let rec collect_fv_from_term = function
  24   | A.Constant name -> []
  25   | A.Variable name -> [name]
  26   | A.Function (_,l) ->
  27       List.flatten (List.map collect_fv_from_term l)
  28 ;;
  29
  30 let collect_arities_from_atom a =
  31   let aux = function
  32     | A.Proposition name -> assert false
  33     | A.Predicate _ -> assert false
  34     | A.True -> []
  35     | A.False -> []
  36     | A.Eq (t1,t2) -> collect_arities_from_term t1 @ collect_arities_from_term t2
  37     | A.NotEq (t1,t2) -> collect_arities_from_term t1 @ collect_arities_from_term t2
  38   in
  39   aux a
  40 ;;
  41
  42 let collect_fv_from_atom a =
  43   let aux = function
  44     | A.Proposition name -> assert false
  45     | A.Predicate _ -> assert false
  46     | A.True -> []
  47     | A.False -> []
  48     | A.Eq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2
  49     | A.NotEq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2
  50   in
  51   HExtlib.list_uniq (List.sort compare (aux a))
  52 ;;
  53
  54 let rec convert_term = function
  55   | A.Variable x -> mk_ident x
  56   | A.Constant x -> mk_ident x
  57   | A.Function (name, args) ->
  58       PT.Appl (mk_ident name :: List.map convert_term args)
  59 ;;
  60
  61 let atom_of_formula = function
  62     | A.Disjunction _ -> assert false
  63     | A.NegAtom a -> a (* removes the negation *)
  64     | A.Atom a -> a
  65 ;;
  66
  67 let rec mk_arrow component = function
  68   | 0 -> mk_ident component
  69   | n ->
  70       PT.Binder
  71         (`Forall,
  72           ((mk_ident "_"),Some (mk_ident component)),
  73           mk_arrow component (n-1))
  74 ;;
  75
  76 let build_ctx_for_arities arities t =
  77   let rec aux = function
  78     | [] -> t
  79     | (name,nargs)::tl ->
  80         PT.Binder
  81           (`Forall,
  82             (mk_ident name,Some (mk_arrow "A" nargs)),
  83             aux tl)
  84   in
  85   aux arities
  86 ;;
  87
  88 let convert_atom a =
  89   let aux = function
  90   | A.Proposition _ -> assert false
  91   | A.Predicate (name,params) ->
  92       prerr_endline ("Predicate is unsupported: " ^ name);
  93       assert false
  94   | A.True -> mk_ident "True"
  95   | A.False -> mk_ident "False"
  96   | A.Eq (l,r)
  97   | A.NotEq (l,r) -> (* removes the negation *)
  98       PT.Appl [mk_ident "eq";mk_ident "A";convert_term l;convert_term r]
  99   in
 100   build_ctx_for_arities (List.map (fun x -> (x,0)) (collect_fv_from_atom a)) (aux a)
 101 ;;
 102
 103 let collect_arities atom ctx =
 104   let atoms = atom::(List.map atom_of_formula ctx) in
 105   HExtlib.list_uniq (List.sort (fun (a,_) (b,_) -> compare a b)
 106     (List.flatten (List.map collect_arities_from_atom atoms)))
 107 ;;
 108
 109 let rec convert_formula no_arities context f =
 110   let atom = atom_of_formula f in
 111   let t = convert_atom atom in
 112   let rec build_ctx n = function
 113     | [] -> t
 114     | hp::tl ->
 115         PT.Binder
 116           (`Forall,
 117             (mk_ident ("H" ^ string_of_int n),
 118                        Some (convert_formula true [] hp)),
 119             build_ctx (n+1) tl)
 120   in
 121   let arities = if no_arities then [] else collect_arities atom context in
 122   build_ctx_for_arities arities (build_ctx 0 context)
 123 ;;
 124
 125 let convert_ast statements context = function
 126   | A.Comment s ->
 127       let s = String.sub s 1 (String.length s - 1) in
 128       let s =
 129         if s.[String.length s - 1] = '\n' then
 130           String.sub s 0 (String.length s - 1)
 131         else
 132           s
 133       in
 134       statements @ [GA.Comment (floc,GA.Note (floc,s))],
 135       context
 136   | A.Inclusion (s,_) ->
 137       statements @ [
 138         GA.Comment (
 139           floc, GA.Note (
 140             floc,"Inclusion of: " ^ s))], context
 141   | A.AnnotatedFormula (name,kind,f,_,_) ->
 142       match kind with
 143       | A.Axiom
 144       | A.Hypothesis ->
 145           statements, f::context
 146       | A.Negated_conjecture ->
 147           let f =
 148             PT.Binder
 149              (`Forall,
 150                (mk_ident "A",Some (PT.Sort `Set)),
 151                convert_formula false context f)
 152           in
 153           let o = PT.Theorem (`Theorem,name,f,None) in
 154           statements @ [
 155             GA.Executable(floc,GA.Command(floc,GA.Obj(floc,o)));
 156             GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
 157               GA.Intros (floc,None,[])),Some (GA.Dot(floc))));
 158             GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
 159               GA.Auto (floc,None,None,Some "paramodulation",None)),
 160                 Some (GA.Dot(floc))));
 161             GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))],
 162           context
 163       | A.Definition
 164       | A.Lemma
 165       | A.Theorem
 166       | A.Conjecture
 167       | A.Lemma_conjecture
 168       | A.Plain
 169       | A.Unknown -> assert false
 170 ;;
 171
 172 (* OPTIONS *)
 173 let tptppath = ref "./";;
 174 let librarymode = ref false;;
 175 let spec = [
 176   ("-tptppath",
 177       Arg.String (fun x -> tptppath := x),
 178       "Where to find the Axioms/ and Problems/ directory");
 179   ("-librarymode",
 180       Arg.Set librarymode,
 181       "... not supported yet")
 182 ]
 183
 184 (* HELPERS *)
 185 let resolve s =
 186   let resolved_name =
 187     if Filename.check_suffix s ".p" then
 188       (assert (String.length s > 5);
 189       let prefix = String.sub s 0 3 in
 190       !tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
 191     else
 192       !tptppath ^ "/" ^ s
 193   in
 194   if HExtlib.is_regular resolved_name then
 195     resolved_name
 196   else
 197     begin
 198       prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
 199       exit 1
 200     end
 201 ;;
 202
 203 (* MAIN *)
 204 let _ =
 205   let usage = "Usage: tptp2grafite [options] file" in
 206   let inputfile = ref "" in
 207   Arg.parse spec (fun s -> inputfile := s) usage;
 208   if !inputfile = "" then
 209     begin
 210       prerr_endline usage;
 211       exit 1
 212     end;
 213   let rec aux = function
 214     | [] -> []
 215     | ((A.Inclusion (file,_)) as hd) :: tl ->
 216         let file = resolve file in
 217         let lexbuf = Lexing.from_channel (open_in file) in
 218         let statements = Parser.main Lexer.yylex lexbuf in
 219         hd :: aux (statements @ tl)
 220     | hd::tl -> hd :: aux tl
 221   in
 222   let statements = aux [A.Inclusion (!inputfile ^ ".p",[])] in
 223   let grafite_ast_statements,_ =
 224     List.fold_left
 225       (fun (st, ctx) f ->
 226         let newst, ctx = convert_ast st ctx f in
 227         newst, ctx)
 228       ([],[]) statements
 229   in
 230   let pp t =
 231     (* for a correct pp we should disambiguate the term... *)
 232     let term_pp = CicNotationPp.pp_term in
 233     let lazy_term_pp = fun x -> assert false in
 234     let obj_pp = CicNotationPp.pp_obj in
 235     print_endline
 236       (GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t)
 237   in
 238   let extra_statements_start = [
 239     GA.Executable(floc,GA.Command(floc,
 240       GA.Set(floc,"baseuri","cic:/matita/TPTP/" ^ !inputfile)));
 241     GA.Executable(floc,GA.Command(floc, GA.Include(floc,"legacy/coq.ma")))]
 242   in
 243   List.iter pp extra_statements_start;
 244   print_endline
 245     (LexiconAstPp.pp_command
 246       (LA.Alias(floc,
 247         LA.Ident_alias("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"))) ^ ".");
 248   List.iter pp grafite_ast_statements;
 249   exit 0