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 neg pos = function
  88     | A.Disjunction (a,b) ->
  89         let neg, pos = atom_of_formula neg pos a in
  90         atom_of_formula neg pos b
  91     | A.NegAtom a -> a::neg, pos
  92     | A.Atom (A.NotEq (a,b)) -> (A.Eq (a,b) :: neg), pos
  93     | A.Atom a -> neg, a::pos
  94 ;;
  95
  96 let atom_of_formula f =
  97   let neg, pos = atom_of_formula [] [] f in
  98   neg @ pos
  99 ;;
 100
 101 let rec mk_arrow component tail = function
 102   | 0 -> begin
 103       match tail with
 104       | Prop -> mk_ident prop
 105       | Univ -> mk_ident universe
 106       end
 107   | n ->
 108       PT.Binder
 109         (`Forall,
 110           ((mk_ident "_"),Some (mk_ident component)),
 111           mk_arrow component tail (n-1))
 112 ;;
 113
 114 let build_ctx_for_arities univesally arities t =
 115   let binder = if univesally then `Forall else `Exists in
 116   let rec aux = function
 117     | [] -> t
 118     | (name,(nargs,sort))::tl ->
 119         PT.Binder
 120           (binder,
 121             (mk_ident name,Some (mk_arrow universe sort nargs)),
 122             aux tl)
 123   in
 124   aux arities
 125 ;;
 126
 127 let convert_atom universally a =
 128   let aux = function
 129   | A.Proposition p -> mk_ident p
 130   | A.Predicate (name,params) ->
 131       PT.Appl ((mk_ident name) :: (List.map convert_term params))
 132   | A.True -> mk_ident "True"
 133   | A.False -> mk_ident "False"
 134   | A.Eq (l,r)
 135   | A.NotEq (l,r) -> (* removes the negation *)
 136       PT.Appl [mk_ident "eq";mk_ident universe;convert_term l;convert_term r]
 137   in
 138   let rec aux2 = function
 139     | [] -> assert false
 140     | [x] -> aux x
 141     | he::tl ->
 142         if universally then
 143           PT.Binder (`Forall, (mk_ident "_", Some (aux he)), aux2 tl)
 144         else
 145           PT.Appl [mk_ident "And";aux he;aux2 tl]
 146   in
 147   let arities = collect_arities_from_atom a in
 148   let fv = collect_fv_from_atom a in
 149   build_ctx_for_arities universally
 150     (List.filter
 151       (function (x,(0,Univ)) -> List.mem x fv | _-> false)
 152       arities)
 153     (aux2 a)
 154 ;;
 155
 156 let collect_arities atom ctx =
 157   let atoms = atom@(List.flatten (List.map atom_of_formula ctx)) in
 158   collect_arities_from_atom atoms
 159 ;;
 160
 161 let collect_arities_from_formulae f =
 162   let rec collect_arities_from_formulae = function
 163   | A.Disjunction (a,b) ->
 164       collect_arities_from_formulae a @ collect_arities_from_formulae b
 165   | A.NegAtom a
 166   | A.Atom a -> collect_arities_from_atom [a]
 167   in
 168   HExtlib.list_uniq (List.sort compare (collect_arities_from_formulae f))
 169 ;;
 170
 171 let is_formulae_1eq_negated f =
 172   let atom = atom_of_formula f in
 173   match atom with
 174   | [A.NotEq (l,r)] -> true
 175   | _ -> false
 176 ;;
 177
 178 let collect_fv_1stord_from_formulae f =
 179   let arities = collect_arities_from_formulae f in
 180   let fv = collect_fv_from_formulae f in
 181   List.map fst
 182     (List.filter (function (x,(0,Univ)) -> List.mem x fv | _-> false) arities)
 183 ;;
 184
 185 let rec convert_formula fv no_arities context f =
 186   let atom = atom_of_formula f in
 187   let t = convert_atom (fv = []) atom in
 188   let rec build_ctx n = function
 189     | [] -> t
 190     | hp::tl ->
 191         PT.Binder
 192           (`Forall,
 193             (mk_ident ("H" ^ string_of_int n),
 194               Some (convert_formula [] true [] hp)),
 195             build_ctx (n+1) tl)
 196   in
 197   let arities = if no_arities then [] else collect_arities atom context in
 198   build_ctx_for_arities true arities (build_ctx 0 context)
 199 ;;
 200
 201 let check_if_atom_is_negative = function
 202   | A.True -> false
 203   | A.False -> true
 204   | A.Proposition _ -> false
 205   | A.Predicate _ -> false
 206   | A.Eq _ -> false
 207   | A.NotEq _ -> true
 208 ;;
 209
 210 let rec check_if_formula_is_negative = function
 211   | A.Disjunction (a,b) ->
 212       check_if_formula_is_negative a && check_if_formula_is_negative b
 213   | A.NegAtom a -> not (check_if_atom_is_negative a)
 214   | A.Atom a -> check_if_atom_is_negative a
 215 ;;
 216
 217 let ng_generate_tactics fv ueq_case context arities =
 218   [ GA.Executable(floc,GA.NTactic(floc,
 219      [GA.NIntro (floc,"Univ") ; GA.NDot(floc)])) ]
 220   @
 221   (HExtlib.list_mapi
 222    (fun (name,_) _->
 223      GA.Executable(floc,GA.NTactic(floc,
 224       [GA.NIntro (floc,(try List.assoc name kw with Not_found -> name));
 225        GA.NDot(floc)])))
 226    arities)
 227   @
 228   (HExtlib.list_mapi
 229    (fun _ i->
 230      GA.Executable(floc,GA.NTactic(floc,
 231       [GA.NIntro (floc,"H"^string_of_int i);GA.NDot(floc)])))
 232    context)
 233   @
 234 (if fv <> [] then
 235   (List.flatten
 236     (List.map
 237       (fun _ ->
 238         [GA.Executable(floc,GA.NTactic(floc,
 239           [GA.NApply (floc,
 240             PT.Appl
 241              [mk_ident "ex_intro";PT.Implicit `JustOne;PT.Implicit `JustOne;
 242               PT.Implicit `JustOne;PT.Implicit `JustOne]);GA.NBranch floc]));
 243          GA.Executable(floc,GA.NTactic(floc,
 244           [GA.NPos (floc,[2])]))])
 245       fv))
 246  else [])@
 247   [GA.Executable(floc,GA.NTactic(floc, [
 248     if (*ueq_case*) true then
 249         GA.NAuto (floc,(Some
 250           HExtlib.list_mapi
 251             (fun _ i ->
 252                mk_ident ("H" ^ string_of_int i))
 253             context
 254                 ,[]))
 255     else
 256         GA.NAuto (floc,(None,[
 257                 "depth",string_of_int 5;
 258                 "width",string_of_int 5;
 259                 "size",string_of_int 20;
 260                 "timeout",string_of_int 10;
 261         ]))
 262  ;
 263   GA.NSemicolon(floc)]));
 264 (*
 265   GA.Executable(floc,GA.NTactic(floc, Some (GA.Try(floc,
 266     GA.Assumption floc)), GA.Dot(floc)))
 267 *)
 268   ]@
 269 (if fv <> [] then
 270   (List.flatten
 271     (List.map
 272       (fun _ ->
 273               [GA.Executable(floc,GA.NTactic(floc, [GA.NShift floc;
 274                GA.NSkip floc; GA.NMerge floc]))])
 275       fv))
 276  else [])@
 277     [GA.Executable(floc,GA.NTactic(floc,[GA.NTry(floc, GA.NAssumption(floc));
 278                                          GA.NSemicolon(floc)]))]@
 279   [GA.Executable(floc,GA.NCommand(floc, GA.NQed(floc)))]
 280 ;;
 281
 282 let generate_tactics fv ueq_case =
 283   [GA.Executable(floc,GA.Tactic(floc, Some
 284    (GA.Intros (floc,(None,[]))),GA.Dot(floc)))] @
 285 (if fv <> [] then
 286   (List.flatten
 287     (List.map
 288       (fun _ ->
 289         [GA.Executable(floc,GA.Tactic(floc, Some
 290           (GA.Exists floc),GA.Branch floc));
 291          GA.Executable(floc,GA.Tactic(floc, None,
 292           (GA.Pos (floc,[2]))))])
 293       fv))
 294  else [])@
 295   [GA.Executable(floc,GA.Tactic(floc, Some (
 296     if true (*ueq_case*) then
 297         GA.AutoBatch (floc,(None,["paramodulation","";
 298         "timeout",string_of_int !paramod_timeout]))
 299     else
 300         GA.AutoBatch (floc,(None,[
 301                 "depth",string_of_int 5;
 302                 "width",string_of_int 5;
 303                 "size",string_of_int 20;
 304                 "timeout",string_of_int 10;
 305         ]))
 306   ),
 307     GA.Semicolon(floc)));
 308   GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc,
 309     GA.Assumption floc)), GA.Dot(floc)))
 310   ]@
 311 (if fv <> [] then
 312   (List.flatten
 313     (List.map
 314       (fun _ ->
 315         [GA.Executable(floc,GA.Tactic(floc, None, GA.Shift floc));
 316          GA.Executable(floc,GA.NonPunctuationTactical(floc, GA.Skip floc,
 317          (GA.Merge floc)))])
 318       fv))
 319  else [])@
 320   [GA.Executable(floc,GA.Command(floc, GA.Print(floc,"proofterm")));
 321    GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))]
 322 ;;
 323
 324 let convert_ast ng statements context = function
 325   | A.Comment s ->
 326       let s = String.sub s 1 (String.length s - 1) in
 327       let s =
 328         if s.[String.length s - 1] = '\n' then
 329           String.sub s 0 (String.length s - 1)
 330         else
 331           s
 332       in
 333       statements @ [GA.Comment (floc,GA.Note (floc,s))],
 334       context
 335   | A.Inclusion (s,_) ->
 336       statements @ [
 337         GA.Comment (
 338           floc, GA.Note (
 339             floc,"Inclusion of: " ^ s))], context
 340   | A.AnnotatedFormula (name,kind,f,_,_) ->
 341       match kind with
 342       | A.Axiom
 343       | A.Hypothesis ->
 344           statements, f::context
 345       | A.Negated_conjecture when not (check_if_formula_is_negative f) ->
 346           statements, f::context
 347       | A.Negated_conjecture ->
 348           let ueq_case = is_formulae_1eq_negated f in
 349           let fv = collect_fv_1stord_from_formulae f in
 350           let old_f = f in
 351           let f =
 352             PT.Binder
 353              (`Forall,
 354                (mk_ident universe,Some (PT.Sort (`Type (CicUniv.fresh ())))),
 355                convert_formula fv false context f)
 356           in
 357           let o = PT.Theorem (`Theorem,name,f,None,`Regular) in
 358           (statements @
 359           [ GA.Executable(floc,GA.Command(floc,
 360              (*if ng then GA.NObj (floc,o) else*) GA.Obj(floc,o))); ] @
 361           if ng then
 362             ng_generate_tactics fv ueq_case context
 363               (let atom = atom_of_formula old_f in collect_arities atom context)
 364           else generate_tactics fv ueq_case),
 365           context
 366       | A.Definition
 367       | A.Lemma
 368       | A.Theorem
 369       | A.Conjecture
 370       | A.Lemma_conjecture
 371       | A.Plain
 372       | A.Unknown -> assert false
 373 ;;
 374
 375 (* HELPERS *)
 376 let resolve ~tptppath s =
 377   let resolved_name =
 378     if Filename.check_suffix s ".p" then
 379       (assert (String.length s > 5);
 380       let prefix = String.sub s 0 3 in
 381       tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
 382     else
 383       tptppath ^ "/" ^ s
 384   in
 385   if HExtlib.is_regular resolved_name then
 386     resolved_name
 387   else
 388     begin
 389       prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
 390       exit 1
 391     end
 392 ;;
 393
 394 (* MAIN *)
 395 let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filename ~ng () =
 396   paramod_timeout := timeout;
 397   depth := def_depth;
 398   let rec aux = function
 399     | [] -> []
 400     | ((A.Inclusion (file,_)) as hd) :: tl ->
 401         let file = resolve ~tptppath file in
 402         let lexbuf = Lexing.from_channel (open_in file) in
 403         let statements = Parser.main Lexer.yylex lexbuf in
 404         hd :: aux (statements @ tl)
 405     | hd::tl -> hd :: aux tl
 406   in
 407   let statements = aux [A.Inclusion (filename,[])] in
 408   let grafite_ast_statements,_ =
 409     List.fold_left
 410       (fun (st, ctx) f ->
 411         let newst, ctx = convert_ast ng st ctx f in
 412         newst, ctx)
 413       ([],[]) statements
 414   in
 415   let pp t =
 416     (* ZACK: setting width to 80 will trigger a bug of BoxPp.render_to_string
 417      * which will show up using the following command line:
 418      * ./tptp2grafite -tptppath ~tassi/TPTP-v3.1.1 GRP170-1 *)
 419     let width = max_int in
 420     let term_pp prec content_term =
 421       let pres_term = TermContentPres.pp_ast content_term in
 422       let lookup_uri = fun _ -> None in
 423       let markup = CicNotationPres.render ~lookup_uri ~prec pres_term in
 424       let s = BoxPp.render_to_string List.hd width markup ~map_unicode_to_tex:false in
 425       Pcre.substitute
 426        ~rex:(Pcre.regexp ~flags:[`UTF8] "∀[Ha-z][a-z0-9_]*") ~subst:(fun x -> "\n" ^ x)
 427        s
 428     in
 429     CicNotationPp.set_pp_term (term_pp 90);
 430     let lazy_term_pp = fun x -> assert false in
 431     let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
 432     Pcre.replace ~pat:"theorem" ~templ:"ntheorem"
 433      (GrafiteAstPp.pp_statement
 434        ~map_unicode_to_tex:false ~term_pp:(term_pp 19) ~lazy_term_pp ~obj_pp t)
 435   in
 436   let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in
 437   let extra_statements_start = [
 438     (*GA.Executable(floc,GA.Command(floc,
 439     GA.Set(floc,"baseuri",buri)))*)]
 440   in
 441   let preamble =
 442     match raw_preamble with
 443     | None ->
 444       pp
 445        (GA.Executable(floc,
 446          GA.Command(floc,GA.Include(floc,true,`OldAndNew,"logic/equality.ma"))))
 447     | Some s -> s buri
 448   in
 449   let extra_statements_end = [] in
 450   let aliases = []
 451    (*[("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)");
 452    ("trans_eq","cic:/Coq/Init/Logic/trans_eq.con");
 453    ("eq_ind_r","cic:/Coq/Init/Logic/eq_ind_r.con");
 454    ("eq_ind","cic:/Coq/Init/Logic/eq_ind.con");
 455    ("sym_eq","cic:/Coq/Init/Logic/sym_eq.con");
 456    ("refl_equal","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)")] *)
 457   in
 458   let s1 = List.map pp extra_statements_start in
 459   let s2 =
 460     List.map
 461      (fun (n,s) ->
 462        LexiconAstPp.pp_command (LA.Alias(floc, LA.Ident_alias(n,s))) ^ ".")
 463      aliases
 464   in
 465   let s3 = List.map pp grafite_ast_statements in
 466   let s4 = List.map pp extra_statements_end in
 467   String.concat "\n" (s1@[preamble]@s2@s3@s4)
 468 ;;