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 ;;