helm/software/components/binaries/matitaprover/tptp_cnf.ml

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