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