helm/software/components/binaries/tptp2grafite/main.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 kw = [
   8  "and","myand"
   9 ];;
  10
  11 let mk_ident s =
  12   PT.Ident ((try List.assoc s kw with Not_found -> s),None)
  13 ;;
  14
  15 let rec collect_arities_from_term = function
  16   | A.Constant name -> [name,0]
  17   | A.Variable name -> []
  18   | A.Function (name,l) ->
  19       (name,List.length l)::List.flatten (List.map collect_arities_from_term l)
  20 ;;
  21
  22 let rec collect_fv_from_term = function
  23   | A.Constant name -> []
  24   | A.Variable name -> [name]
  25   | A.Function (_,l) ->
  26       List.flatten (List.map collect_fv_from_term l)
  27 ;;
  28
  29 let collect_arities_from_atom a =
  30   let aux = function
  31     | A.Proposition name -> assert false
  32     | A.Predicate _ -> assert false
  33     | A.True -> []
  34     | A.False -> []
  35     | A.Eq (t1,t2) -> collect_arities_from_term t1 @ collect_arities_from_term t2
  36     | A.NotEq (t1,t2) -> collect_arities_from_term t1 @ collect_arities_from_term t2
  37   in
  38   aux a
  39 ;;
  40
  41 let collect_fv_from_atom a =
  42   let aux = function
  43     | A.Proposition name -> assert false
  44     | A.Predicate _ -> assert false
  45     | A.True -> []
  46     | A.False -> []
  47     | A.Eq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2
  48     | A.NotEq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2
  49   in
  50   HExtlib.list_uniq (List.sort compare (aux a))
  51 ;;
  52
  53 let collect_fv_from_formulae = function
  54   | A.Disjunction _ -> assert false
  55   | A.NegAtom a
  56   | A.Atom a -> collect_fv_from_atom a
  57 ;;
  58
  59 let rec convert_term = function
  60   | A.Variable x -> mk_ident x
  61   | A.Constant x -> mk_ident x
  62   | A.Function (name, args) ->
  63       PT.Appl (mk_ident name :: List.map convert_term args)
  64 ;;
  65
  66 let atom_of_formula = function
  67     | A.Disjunction _ -> assert false
  68     | A.NegAtom a -> a (* removes the negation *)
  69     | A.Atom a -> a
  70 ;;
  71
  72 let rec mk_arrow component = function
  73   | 0 -> mk_ident component
  74   | n ->
  75       PT.Binder
  76         (`Forall,
  77           ((mk_ident "_"),Some (mk_ident component)),
  78           mk_arrow component (n-1))
  79 ;;
  80
  81 let build_ctx_for_arities univesally arities t =
  82   let binder = if univesally then `Forall else `Exists in
  83   let rec aux = function
  84     | [] -> t
  85     | (name,nargs)::tl ->
  86         PT.Binder
  87           (binder,
  88             (mk_ident name,Some (mk_arrow "A" nargs)),
  89             aux tl)
  90   in
  91   aux arities
  92 ;;
  93
  94 let convert_atom universally a =
  95   let aux = function
  96   | A.Proposition _ -> assert false
  97   | A.Predicate (name,params) ->
  98       prerr_endline ("Predicate is unsupported: " ^ name);
  99       assert false
 100   | A.True -> mk_ident "True"
 101   | A.False -> mk_ident "False"
 102   | A.Eq (l,r)
 103   | A.NotEq (l,r) -> (* removes the negation *)
 104       PT.Appl [mk_ident "eq";mk_ident "A";convert_term l;convert_term r]
 105   in
 106   build_ctx_for_arities universally
 107     (List.map (fun x -> (x,0)) (collect_fv_from_atom a)) (aux a)
 108 ;;
 109
 110 let collect_arities atom ctx =
 111   let atoms = atom::(List.map atom_of_formula ctx) in
 112   HExtlib.list_uniq (List.sort (fun (a,_) (b,_) -> compare a b)
 113     (List.flatten (List.map collect_arities_from_atom atoms)))
 114 ;;
 115
 116 let assert_formulae_is_1eq_negated f =
 117   let atom = atom_of_formula f in
 118   match atom with
 119   | A.Eq (l,r) -> failwith "Negated formula is not negated"
 120   | A.NotEq (l,r) -> ()
 121   | _ -> failwith "Not a unit equality formula"
 122 ;;
 123
 124 let rec convert_formula fv no_arities context f =
 125   let atom = atom_of_formula f in
 126   let t = convert_atom (fv = []) atom in
 127   let rec build_ctx n = function
 128     | [] -> t
 129     | hp::tl ->
 130         PT.Binder
 131           (`Forall,
 132             (mk_ident ("H" ^ string_of_int n),
 133               Some (convert_formula [] true [] hp)),
 134             build_ctx (n+1) tl)
 135   in
 136   let arities = if no_arities then [] else collect_arities atom context in
 137   build_ctx_for_arities true arities (build_ctx 0 context)
 138 ;;
 139
 140 let check_if_atom_is_negative = function
 141   | A.True | A.False | A.Proposition _ | A.Predicate _ -> assert false
 142   | A.Eq _ -> false
 143   | A.NotEq _ -> true
 144 ;;
 145
 146 let check_if_formula_is_negative = function
 147   | A.Disjunction _ -> assert false
 148   | A.NegAtom a -> not (check_if_atom_is_negative a)
 149   | A.Atom a -> check_if_atom_is_negative a
 150 ;;
 151
 152 let convert_ast statements context = function
 153   | A.Comment s ->
 154       let s = String.sub s 1 (String.length s - 1) in
 155       let s =
 156         if s.[String.length s - 1] = '\n' then
 157           String.sub s 0 (String.length s - 1)
 158         else
 159           s
 160       in
 161       statements @ [GA.Comment (floc,GA.Note (floc,s))],
 162       context
 163   | A.Inclusion (s,_) ->
 164       statements @ [
 165         GA.Comment (
 166           floc, GA.Note (
 167             floc,"Inclusion of: " ^ s))], context
 168   | A.AnnotatedFormula (name,kind,f,_,_) ->
 169       match kind with
 170       | A.Axiom
 171       | A.Hypothesis ->
 172           statements, f::context
 173       | A.Negated_conjecture when not (check_if_formula_is_negative f) ->
 174           statements, f::context
 175       | A.Negated_conjecture ->
 176           assert_formulae_is_1eq_negated f;
 177           let fv = collect_fv_from_formulae f in
 178           if fv <> [] then
 179             prerr_endline ("FREE VARIABLES: " ^ String.concat "," fv);
 180           let f =
 181             PT.Binder
 182              (`Forall,
 183                (mk_ident "A",Some (PT.Sort `Set)),
 184                convert_formula fv false context f)
 185           in
 186           let o = PT.Theorem (`Theorem,name,f,None) in
 187           statements @ [
 188             GA.Executable(floc,GA.Command(floc,GA.Obj(floc,o)));
 189             GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
 190             GA.Intros (floc,None,[])),Some (GA.Dot(floc))))] @
 191           (if fv <> [] then
 192             (List.flatten
 193               (List.map
 194                 (fun _ ->
 195                   [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
 196                     GA.Exists floc),Some (GA.Branch floc)));
 197                    GA.Executable(floc,GA.Tactical(floc, GA.Pos (floc,2),None))])
 198                 fv))
 199            else [])@
 200             [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
 201               GA.Auto (floc,None,None,Some "paramodulation",None)),
 202                 Some (GA.Dot(floc))))]@
 203           (if fv <> [] then
 204             (List.flatten
 205               (List.map
 206                 (fun _ ->
 207                   [GA.Executable(floc,GA.Tactical(floc, GA.Shift floc, None));
 208                    GA.Executable(floc,GA.Tactical(floc, GA.Skip floc,Some
 209                    (GA.Merge floc)))])
 210                 fv))
 211            else [])@
 212             [GA.Executable(floc,GA.Tactical(floc, GA.Try(floc,
 213               GA.Tactic (floc, GA.Assumption floc)), Some (GA.Dot(floc))));
 214             GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))],
 215           context
 216       | A.Definition
 217       | A.Lemma
 218       | A.Theorem
 219       | A.Conjecture
 220       | A.Lemma_conjecture
 221       | A.Plain
 222       | A.Unknown -> assert false
 223 ;;
 224
 225 (* OPTIONS *)
 226 let tptppath = ref "./";;
 227 let librarymode = ref false;;
 228 let spec = [
 229   ("-tptppath",
 230       Arg.String (fun x -> tptppath := x),
 231       "Where to find the Axioms/ and Problems/ directory");
 232   ("-librarymode",
 233       Arg.Set librarymode,
 234       "... not supported yet")
 235 ]
 236
 237 (* HELPERS *)
 238 let resolve s =
 239   let resolved_name =
 240     if Filename.check_suffix s ".p" then
 241       (assert (String.length s > 5);
 242       let prefix = String.sub s 0 3 in
 243       !tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
 244     else
 245       !tptppath ^ "/" ^ s
 246   in
 247   if HExtlib.is_regular resolved_name then
 248     resolved_name
 249   else
 250     begin
 251       prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
 252       exit 1
 253     end
 254 ;;
 255
 256 (* MAIN *)
 257 let _ =
 258   let usage = "Usage: tptp2grafite [options] file" in
 259   let inputfile = ref "" in
 260   Arg.parse spec (fun s -> inputfile := s) usage;
 261   if !inputfile = "" then
 262     begin
 263       prerr_endline usage;
 264       exit 1
 265     end;
 266   let rec aux = function
 267     | [] -> []
 268     | ((A.Inclusion (file,_)) as hd) :: tl ->
 269         let file = resolve file in
 270         let lexbuf = Lexing.from_channel (open_in file) in
 271         let statements = Parser.main Lexer.yylex lexbuf in
 272         hd :: aux (statements @ tl)
 273     | hd::tl -> hd :: aux tl
 274   in
 275   let statements = aux [A.Inclusion (!inputfile ^ ".p",[])] in
 276   let grafite_ast_statements,_ =
 277     List.fold_left
 278       (fun (st, ctx) f ->
 279         let newst, ctx = convert_ast st ctx f in
 280         newst, ctx)
 281       ([],[]) statements
 282   in
 283   let pp t =
 284     (* for a correct pp we should disambiguate the term... *)
 285     let term_pp = CicNotationPp.pp_term in
 286     let lazy_term_pp = fun x -> assert false in
 287     let obj_pp = CicNotationPp.pp_obj in
 288     print_endline
 289       (GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t)
 290   in
 291   let extra_statements_start = [
 292     GA.Executable(floc,GA.Command(floc,
 293       GA.Set(floc,"baseuri","cic:/matita/TPTP/" ^ !inputfile)));
 294     GA.Executable(floc,GA.Command(floc, GA.Include(floc,"legacy/coq.ma")))]
 295   in
 296   List.iter pp extra_statements_start;
 297   print_endline
 298     (LexiconAstPp.pp_command
 299       (LA.Alias(floc,
 300         LA.Ident_alias("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"))) ^ ".");
 301   List.iter pp grafite_ast_statements;
 302   exit 0