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 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 (*
 181           if fv <> [] then
 182             prerr_endline ("FREE VARIABLES: " ^ String.concat "," fv);
 183 *)
 184           let f =
 185             PT.Binder
 186              (`Forall,
 187                (mk_ident universe,Some (PT.Sort `Set)),
 188                convert_formula fv false context f)
 189           in
 190           let o = PT.Theorem (`Theorem,name,f,None) in
 191           statements @ [
 192             GA.Executable(floc,GA.Command(floc,GA.Obj(floc,o)));
 193             GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
 194             GA.Intros (floc,None,[])),Some (GA.Dot(floc))))] @
 195           (if fv <> [] then
 196             (List.flatten
 197               (List.map
 198                 (fun _ ->
 199                   [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
 200                     GA.Exists floc),Some (GA.Branch floc)));
 201                    GA.Executable(floc,GA.Tactical(floc,
 202                     GA.Pos (floc,[2]),None))])
 203                 fv))
 204            else [])@
 205             [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
 206             GA.Auto (floc,["paramodulation",""])),
 207               Some (GA.Dot(floc))));
 208             GA.Executable(floc,GA.Tactical(floc, GA.Try(floc,
 209               GA.Tactic (floc, GA.Assumption floc)), Some (GA.Dot(floc))))
 210             ]@
 211           (if fv <> [] then
 212             (List.flatten
 213               (List.map
 214                 (fun _ ->
 215                   [GA.Executable(floc,GA.Tactical(floc, GA.Shift floc, None));
 216                    GA.Executable(floc,GA.Tactical(floc, GA.Skip floc,Some
 217                    (GA.Merge floc)))])
 218                 fv))
 219            else [])@
 220             [GA.Executable(floc,GA.Command(floc, GA.Print(floc,"proofterm")));
 221              GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))],
 222           context
 223       | A.Definition
 224       | A.Lemma
 225       | A.Theorem
 226       | A.Conjecture
 227       | A.Lemma_conjecture
 228       | A.Plain
 229       | A.Unknown -> assert false
 230 ;;
 231
 232 (* HELPERS *)
 233 let resolve ~tptppath s =
 234   let resolved_name =
 235     if Filename.check_suffix s ".p" then
 236       (assert (String.length s > 5);
 237       let prefix = String.sub s 0 3 in
 238       tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
 239     else
 240       tptppath ^ "/" ^ s
 241   in
 242   if HExtlib.is_regular resolved_name then
 243     resolved_name
 244   else
 245     begin
 246       prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
 247       exit 1
 248     end
 249 ;;
 250
 251 (* MAIN *)
 252 let tptp2grafite ?raw_preamble ~tptppath ~filename () =
 253   let rec aux = function
 254     | [] -> []
 255     | ((A.Inclusion (file,_)) as hd) :: tl ->
 256         let file = resolve ~tptppath file in
 257         let lexbuf = Lexing.from_channel (open_in file) in
 258         let statements = Parser.main Lexer.yylex lexbuf in
 259         hd :: aux (statements @ tl)
 260     | hd::tl -> hd :: aux tl
 261   in
 262   let statements = aux [A.Inclusion (filename,[])] in
 263   let grafite_ast_statements,_ =
 264     List.fold_left
 265       (fun (st, ctx) f ->
 266         let newst, ctx = convert_ast st ctx f in
 267         newst, ctx)
 268       ([],[]) statements
 269   in
 270   let pp t =
 271     (* ZACK: setting width to 80 will trigger a bug of BoxPp.render_to_string
 272      * which will show up using the following command line:
 273      * ./tptp2grafite -tptppath ~tassi/TPTP-v3.1.1 GRP170-1 *)
 274     let width = max_int in
 275     let term_pp content_term =
 276       let pres_term = TermContentPres.pp_ast content_term in
 277       let dummy_tbl = Hashtbl.create 1 in
 278       let markup = CicNotationPres.render dummy_tbl pres_term in
 279       let s = BoxPp.render_to_string List.hd width markup in
 280       Pcre.substitute
 281         ~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s
 282     in
 283     CicNotationPp.set_pp_term term_pp;
 284     let lazy_term_pp = fun x -> assert false in
 285     let obj_pp = CicNotationPp.pp_obj in
 286     GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t
 287   in
 288   let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in
 289   let extra_statements_start = [
 290     GA.Executable(floc,GA.Command(floc,
 291     GA.Set(floc,"baseuri",buri)))]
 292   in
 293   let preamble =
 294     match raw_preamble with
 295     | None ->
 296        pp (GA.Executable(floc,
 297            GA.Command(floc,GA.Include(floc,"logic/equality.ma"))))
 298     | Some s -> s buri
 299   in
 300   let extra_statements_end = [] in
 301   let aliases = []
 302    (*[("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)");
 303    ("trans_eq","cic:/Coq/Init/Logic/trans_eq.con");
 304    ("eq_ind_r","cic:/Coq/Init/Logic/eq_ind_r.con");
 305    ("eq_ind","cic:/Coq/Init/Logic/eq_ind.con");
 306    ("sym_eq","cic:/Coq/Init/Logic/sym_eq.con");
 307    ("refl_equal","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)")] *)
 308   in
 309   let s1 = List.map pp extra_statements_start in
 310   let s2 =
 311     List.map
 312      (fun (n,s) ->
 313        LexiconAstPp.pp_command (LA.Alias(floc, LA.Ident_alias(n,s))) ^ ".")
 314      aliases
 315   in
 316   let s3 = List.map pp grafite_ast_statements in
 317   let s4 = List.map pp extra_statements_end in
 318   String.concat "\n" (s1@[preamble]@s2@s3@s4)
 319 ;;