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