1 module GA = GrafiteAst;;
2 module LA = LexiconAst;;
3 module PT = CicNotationPt;;
5 let floc = HExtlib.dummy_floc;;
7 let rec collect_arities_from_term = function
8 | A.Constant name -> [name,0]
9 | A.Variable name -> []
10 | A.Function (name,l) ->
11 (name,List.length l) :: List.flatten (List.map collect_arities_from_term l)
14 let rec collect_fv_from_term = function
15 | A.Constant name -> []
16 | A.Variable name -> [name]
18 List.flatten (List.map collect_fv_from_term l)
21 let collect_arities_from_atom a =
23 | A.Proposition name -> assert false
24 | A.Predicate _ -> assert false
27 | A.Eq (t1,t2) -> collect_arities_from_term t1 @ collect_arities_from_term t2
28 | A.NotEq (t1,t2) -> collect_arities_from_term t1 @ collect_arities_from_term t2
33 let collect_fv_from_atom a =
35 | A.Proposition name -> assert false
36 | A.Predicate _ -> assert false
39 | A.Eq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2
40 | A.NotEq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2
42 HExtlib.list_uniq (List.sort compare (aux a))
45 let rec convert_term = function
46 | A.Variable x -> PT.Ident (x,None)
47 | A.Constant x -> PT.Ident (x,None)
48 | A.Function (name, args) ->
49 PT.Appl (PT.Ident (name,None) :: List.map convert_term args)
52 let atom_of_formula = function
53 | A.Disjunction _ -> assert false
54 | A.NegAtom a -> a (* removes the negation *)
58 let rec mk_arrow component = function
59 | 0 -> PT.Ident (component,None)
63 ((PT.Ident ("_",None)),Some (PT.Ident (component,None))),
64 mk_arrow component (n-1))
67 let build_ctx_for_arities arities t =
68 let rec aux = function
73 (PT.Ident (name,None),Some (mk_arrow "A" nargs)),
81 | A.Proposition _ -> assert false
82 | A.Predicate (name,params) -> assert false
83 | A.True -> PT.Ident ("True",None)
84 | A.False -> PT.Ident ("False",None)
86 | A.NotEq (l,r) -> (* removes the negation *)
88 PT.Ident ("eq",None); PT.Ident ("A",None); convert_term l; convert_term r]
90 build_ctx_for_arities (List.map (fun x -> (x,0)) (collect_fv_from_atom a)) (aux a)
93 let collect_arities atom ctx =
94 let atoms = atom::(List.map atom_of_formula ctx) in
95 HExtlib.list_uniq (List.sort (fun (a,_) (b,_) -> compare a b)
96 (List.flatten (List.map collect_arities_from_atom atoms)))
99 let rec convert_formula no_arities context f =
100 let atom = atom_of_formula f in
101 let t = convert_atom atom in
102 let rec build_ctx n = function
107 (PT.Ident ("H" ^ string_of_int n,None),
108 Some (convert_formula true [] hp)),
111 let arities = if no_arities then [] else collect_arities atom context in
112 build_ctx_for_arities arities (build_ctx 0 context)
115 let convert_ast statements context = function
117 let s = String.sub s 1 (String.length s - 1) in
119 if s.[String.length s - 1] = '\n' then
120 String.sub s 0 (String.length s - 1)
124 statements @ [GA.Comment (floc,GA.Note (floc,s))],
126 | A.Inclusion (s,_) ->
130 floc,"Inclusion of: " ^ s))], context
131 | A.AnnotatedFormula (name,kind,f,_,_) ->
135 statements, f::context
136 | A.Negated_conjecture ->
140 (PT.Ident ("A",None),Some (PT.Sort `Set)),
141 convert_formula false context f)
143 let o = PT.Theorem (`Theorem,name,f,None) in
147 floc,GA.Obj(floc,o)))],
155 | A.Unknown -> assert false
159 let tptppath = ref "./";;
160 let librarymode = ref false;;
163 Arg.String (fun x -> tptppath := x),
164 "Where to find the Axioms/ and Problems/ directory");
167 "... not supported yet")
173 if Filename.check_suffix s ".p" then
174 (assert (String.length s > 5);
175 let prefix = String.sub s 0 3 in
176 !tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
180 if HExtlib.is_regular resolved_name then
184 prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
191 let usage = "Usage: tptp2grafite [options] file" in
192 let inputfile = ref "" in
193 Arg.parse spec (fun s -> inputfile := s) usage;
194 if !inputfile = "" then
199 let rec aux = function
201 | ((A.Inclusion (file,_)) as hd) :: tl ->
202 let file = resolve file in
203 let lexbuf = Lexing.from_channel (open_in file) in
204 let statements = Parser.main Lexer.yylex lexbuf in
205 hd :: aux (statements @ tl)
206 | hd::tl -> hd :: aux tl
208 let statements = aux [A.Inclusion (!inputfile ^ ".p",[])] in
209 let grafite_ast_statements,_ =
212 let newst, ctx = convert_ast st ctx f in
217 (* for a correct pp we should disambiguate the term... *)
218 let term_pp = CicNotationPp.pp_term in
219 let lazy_term_pp = fun x -> assert false in
220 let obj_pp = CicNotationPp.pp_obj in
222 (GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t)
224 let extra_statements_start = [
225 GA.Executable(floc,GA.Command(floc,
226 GA.Set(floc,"baseuri","cic:/matita/TPTP/" ^ !inputfile)));
227 GA.Executable(floc,GA.Command(floc, GA.Include(floc,"legacy/coq.ma")))]
229 let extra_statements_end = [
230 GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
231 GA.Intros (floc,None,[])),Some (GA.Dot(floc))));
232 GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
233 GA.Auto (floc,None,None,Some "paramodulation",None)),
234 Some (GA.Dot(floc))));
235 GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))]
237 List.iter pp extra_statements_start;
239 (LexiconAstPp.pp_command
241 LA.Ident_alias("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"))) ^ ".");
242 List.iter pp grafite_ast_statements;
243 List.iter pp extra_statements_end;