1 module GA = GrafiteAst;;
2 module LA = LexiconAst;;
3 module PT = CicNotationPt;;
5 let floc = HExtlib.dummy_floc;;
12 PT.Ident ((try List.assoc s kw with Not_found -> s),None)
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)
23 let rec collect_fv_from_term = function
24 | A.Constant name -> []
25 | A.Variable name -> [name]
27 List.flatten (List.map collect_fv_from_term l)
30 let collect_arities_from_atom a =
32 | A.Proposition name -> assert false
33 | A.Predicate _ -> assert 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
42 let collect_fv_from_atom a =
44 | A.Proposition name -> assert false
45 | A.Predicate _ -> assert 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
51 HExtlib.list_uniq (List.sort compare (aux a))
54 let collect_fv_from_formulae = function
55 | A.Disjunction _ -> assert false
57 | A.Atom a -> collect_fv_from_atom a
60 let rec convert_term = function
61 | A.Variable x -> mk_ident x
62 | A.Constant x -> mk_ident x
63 | A.Function (name, args) ->
64 PT.Appl (mk_ident name :: List.map convert_term args)
67 let atom_of_formula = function
68 | A.Disjunction _ -> assert false
69 | A.NegAtom a -> a (* removes the negation *)
73 let rec mk_arrow component = function
74 | 0 -> mk_ident component
78 ((mk_ident "_"),Some (mk_ident component)),
79 mk_arrow component (n-1))
82 let build_ctx_for_arities arities t =
83 let rec aux = function
88 (mk_ident name,Some (mk_arrow "A" nargs)),
96 | A.Proposition _ -> assert false
97 | A.Predicate (name,params) ->
98 prerr_endline ("Predicate is unsupported: " ^ name);
100 | A.True -> mk_ident "True"
101 | A.False -> mk_ident "False"
103 | A.NotEq (l,r) -> (* removes the negation *)
104 PT.Appl [mk_ident "eq";mk_ident "A";convert_term l;convert_term r]
106 build_ctx_for_arities (List.map (fun x -> (x,0)) (collect_fv_from_atom a)) (aux a)
109 let collect_arities atom ctx =
110 let atoms = atom::(List.map atom_of_formula ctx) in
111 HExtlib.list_uniq (List.sort (fun (a,_) (b,_) -> compare a b)
112 (List.flatten (List.map collect_arities_from_atom atoms)))
115 let rec convert_formula no_arities context f =
116 let atom = atom_of_formula f in
117 let t = convert_atom atom in
118 let rec build_ctx n = function
123 (mk_ident ("H" ^ string_of_int n),
124 Some (convert_formula true [] hp)),
127 let arities = if no_arities then [] else collect_arities atom context in
128 build_ctx_for_arities arities (build_ctx 0 context)
131 let convert_ast statements context = function
133 let s = String.sub s 1 (String.length s - 1) in
135 if s.[String.length s - 1] = '\n' then
136 String.sub s 0 (String.length s - 1)
140 statements @ [GA.Comment (floc,GA.Note (floc,s))],
142 | A.Inclusion (s,_) ->
146 floc,"Inclusion of: " ^ s))], context
147 | A.AnnotatedFormula (name,kind,f,_,_) ->
151 statements, f::context
152 | A.Negated_conjecture ->
153 if collect_fv_from_formulae f <> [] then
154 (*prerr_endline "CONTIENE FV";*)();
158 (mk_ident "A",Some (PT.Sort `Set)),
159 convert_formula false context f)
161 let o = PT.Theorem (`Theorem,name,f,None) in
163 GA.Executable(floc,GA.Command(floc,GA.Obj(floc,o)));
164 GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
165 GA.Intros (floc,None,[])),Some (GA.Dot(floc))));
166 GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
167 GA.Auto (floc,None,None,Some "paramodulation",None)),
168 Some (GA.Dot(floc))));
169 GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))],
177 | A.Unknown -> assert false
181 let tptppath = ref "./";;
182 let librarymode = ref false;;
185 Arg.String (fun x -> tptppath := x),
186 "Where to find the Axioms/ and Problems/ directory");
189 "... not supported yet")
195 if Filename.check_suffix s ".p" then
196 (assert (String.length s > 5);
197 let prefix = String.sub s 0 3 in
198 !tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
202 if HExtlib.is_regular resolved_name then
206 prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
213 let usage = "Usage: tptp2grafite [options] file" in
214 let inputfile = ref "" in
215 Arg.parse spec (fun s -> inputfile := s) usage;
216 if !inputfile = "" then
221 let rec aux = function
223 | ((A.Inclusion (file,_)) as hd) :: tl ->
224 let file = resolve file in
225 let lexbuf = Lexing.from_channel (open_in file) in
226 let statements = Parser.main Lexer.yylex lexbuf in
227 hd :: aux (statements @ tl)
228 | hd::tl -> hd :: aux tl
230 let statements = aux [A.Inclusion (!inputfile ^ ".p",[])] in
231 let grafite_ast_statements,_ =
234 let newst, ctx = convert_ast st ctx f in
239 (* for a correct pp we should disambiguate the term... *)
240 let term_pp = CicNotationPp.pp_term in
241 let lazy_term_pp = fun x -> assert false in
242 let obj_pp = CicNotationPp.pp_obj in
244 (GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t)
246 let extra_statements_start = [
247 GA.Executable(floc,GA.Command(floc,
248 GA.Set(floc,"baseuri","cic:/matita/TPTP/" ^ !inputfile)));
249 GA.Executable(floc,GA.Command(floc, GA.Include(floc,"legacy/coq.ma")))]
251 List.iter pp extra_statements_start;
253 (LexiconAstPp.pp_command
255 LA.Ident_alias("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"))) ^ ".");
256 List.iter pp grafite_ast_statements;