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