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