helm/software/components/tptp_grafite/tptp2grafite.ml

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