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