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