tptp2why now linked against the why static library, to use

why AST and pretty-printing facilities
implementation not yet complete

Makefile.in

@@ -392,13 +392,12 @@ clean::
 # Tptp2why
 ########
 
-# TODO : autoconf
-MENHIR=/usr/bin/menhir
+MENHIR=@MENHIR@
 
 TPTPGENERATED = src/tptp2why/tptp_lexer.ml \
 	src/tptp2why/tptp_parser.ml src/tptp2why/tptp_parser.mli
 
-TPTP_FILES = tptpTree tptp_parser tptp_lexer tptp2why
+TPTP_FILES = tptpTree tptp_parser tptp_lexer tptpTranslate tptp2why
 TPTP_DIR=src/tptp2why/
 
 TPTPMODULES = $(addprefix $(TPTP_DIR), $(TPTP_FILES))
@@ -408,7 +407,7 @@ TPTPMLI = $(addsuffix .mli, $(TPTPMODULES))
 TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
 TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
 
-$(TPTPCMO) $(TPTPCMX): INCLUDES = -I $(TPTP_DIR)
+$(TPTPCMO) $(TPTPCMX): INCLUDES = -I $(TPTP_DIR) -I src/core/
 
 # build targets
 
@@ -417,17 +416,16 @@ byte: bin/tptp2why.byte
 opt:  bin/tptp2why.opt
 endif
 
-src/tptp2why/tptp_parser.ml src/tptp2why/tptp_parser.mli: src/tptp2why/tptpTree.cmi src/tptp2why/tptp_parser.mly
-	cd $(TPTP_DIR) && $(MENHIR) --infer tptp_parser.mly
+src/tptp2why/tptp_parser.ml src/tptp2why/tptp_parser.mli: OCAMLYACC = $(MENHIR)
 
-bin/tptp2why.opt: $(TPTPCMX)
+bin/tptp2why.opt: src/why.cmxa $(TPTPCMX)
 	$(if $(QUIET), @echo 'Linking  $@' &&) \
-	    $(OCAMLOPT) $(OFLAGS) -o $@ $^
+	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
 	$(STRIP) $@
 
-bin/tptp2why.byte: $(TPTPCMO)
+bin/tptp2why.byte: src/why.cma $(TPTPCMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
-	    $(OCAMLC) $(BFLAGS) -o $@ $^
+	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
 
 # depend and clean targets
 

src/tptp2why/tptp2why.ml

@@ -2,19 +2,7 @@
 
 open TptpTree
 
-(** very basic name sanitizer for axioms and goals *)
-let sanitize =
-  let module M = Map.Make(struct type t=string let compare = String.compare end) in
-  let m = ref M.empty in
-  fun name -> if M.mem name !m
-    then begin
-      let cur = M.find name !m in
-      m := M.add name (cur+1) !m;
-      name ^ (string_of_int cur)
-    end else begin
-      m := M.add name 0 !m;
-      name
-    end
+open Why
 
 
 module S = Set.Make(struct type t=string let compare = String.compare end)
@@ -75,105 +63,14 @@ end = struct
 
 end
 
-(** basic printer to .why *)
-module Print : sig
 
-  val printDecl : Format.formatter -> decl -> unit
-  val printFmla : Format.formatter -> fmla -> unit
-  val printTheory : Format.formatter -> string -> decl list -> unit
-  val printFile : Format.formatter -> string -> string -> string -> unit
+(* TODO : update code *)
+(** module to process a single file *)
+module Process : sig
 
-end = struct
+  val printFile : Format.formatter -> string -> string -> string -> unit
 
-  open Format
-
-  let show_type ty = match ty with
-  | Axiom -> "axiom"
-  | Conjecture -> "goal"
-
-  let show_fbinop op = match op with
-  | And -> "and"
-  | Or -> "or"
-  | Implies -> "->"
-  | Equiv -> "<->"
-
-  let show_funop = function
-  | Not -> "not"
-
-  let show_tbinop = function
-  | Equal -> "="
-  | NotEqual -> "<>"
-
-  let show_quantifier = function
-  | Forall -> "forall"
-  | Exist -> "exists"
-
-  (** prints a list of items with printer *)
-  let rec print_list ?sep:(sep=", ") printer fmter = function
-  | x::xs when xs <> [] -> fprintf fmter "%a%s%a" printer x sep
-      (print_list ~sep:sep printer) xs
-  | x::[] -> fprintf fmter "%a" printer x
-  | [] -> ()
-  | _ -> assert false
-
-  let printVar fmter v = pp_print_string fmter (String.uncapitalize v)
-  let printAtom fmter a = pp_print_string fmter (String.uncapitalize a)
-
-  let rec printTerm fmter = function
-  | TAtom atom -> printAtom fmter atom
-  | TConst c -> pp_print_string fmter c
-  | TVar v -> printVar fmter v
-  | TFunctor (atom, terms) ->
-    fprintf fmter "@[%s(%a)@]" atom (print_list printTerm) terms
-
-  let rec printFmla fmter = function
-  | FBinop (op, f1, f2) ->
-    fprintf fmter "(@[%a@ %s %a@])" printFmla f1 (show_fbinop op) printFmla f2
-  | FUnop (op, f) ->
-    fprintf fmter "@[(%s %a)@]" (show_funop op) printFmla f
-  | FQuant (quant, vars, f) ->
-    fprintf fmter "%s@ %a : t.@ %a" (show_quantifier quant)
-      (print_list printVar) vars printFmla f
-  | FPred (pred, terms) ->
-    fprintf fmter "%s(@[%a@])" pred (print_list printTerm) terms
-  | FTermBinop (op, t1, t2) ->
-    fprintf fmter "(@[%a %s %a@])" printTerm t1 (show_tbinop op) printTerm t2
-
-
-  let printDecl fmter = function
-  | Fof (name, ty, fmla) ->
-    fprintf fmter "%s %s :@\n @[%a@]\n" (show_type ty)
-      (sanitize (String.capitalize name)) printFmla fmla
-  | Include _ -> failwith "no include should remain here !"
-
-  (** prints the declaration of a functor : logic f(t, t, t... t) *)
-  let printFunctorDecl fmter (f,(ty,arity)) =
-    let ty_print = match ty with Summary.Pred -> "" | Summary.Term -> ":t" in
-    let rec helper fmter arity = match arity with
-    | 0 -> pp_print_string fmter "" | 1 -> pp_print_string fmter "t"
-    | arity -> fprintf fmter "%s, %a" "t" helper (arity-1) in
-    fprintf fmter "logic %a(%a) %s" pp_print_string f helper arity ty_print
-
-  let printAtomDecl fmter atom =
-    fprintf fmter "logic %s : t" (String.uncapitalize atom)
-
-  (** prints forward declarations *)
-  let printPreambule fmter decls =
-    let functors = Summary.findAllFunctors decls in
-    let atoms = Summary.findAllAtoms decls in
-    begin
-      fprintf fmter "type t\n";
-      print_list ~sep:"\n" printAtomDecl fmter (S.fold (fun x y->x::y) atoms []);
-      fprintf fmter "\n\n";
-      print_list ~sep:"\n" printFunctorDecl fmter
-        (M.fold (fun x y acc -> (x,y)::acc) functors []);
-      fprintf fmter "\n\n"
-    end
-
-  (** create a theory with name @name@ and a type t*)
-  let printTheory fmter name decls =
-    fprintf fmter "theory %s@\n@[<hov 2>%a %a@]@\nend\n\n"
-        name printPreambule decls (print_list ~sep:"\n" printDecl) decls
+end= struct
 
   let fromInclude = function | Include x -> x | _ -> assert false
   (** for a given file, returns the list of declarations
@@ -197,7 +94,8 @@ end = struct
   (** process a single file and all includes inside *)
   let printFile fmter include_dir theoryName filename =
     let decls = getAllDecls ~first:true include_dir filename in
-    printTheory fmter theoryName decls
+    let theory = TptpTranslate.theory_of_decls theoryName decls in
+    Pretty.print_theory fmter theory
 
 end
 
@@ -239,5 +137,5 @@ let _ =
   List.iter
     (fun x -> let theoryName = "Theory"^(string_of_int !theoryCounter) in
               incr theoryCounter;
-              Print.printFile !output_chan !include_dir theoryName x)
+              Process.printFile !output_chan !include_dir theoryName x)
     !input_files

src/tptp2why/tptpTranslate.ml

+(** module to translate from the basic abstract tree from the parser
+to a proper why internal representation to be pretty-printed *)
+
+open TptpTree
+
+open Why
+open Why.Ident
+
+(*s this module manages scoping of vars using a stack of
+variables bindings *)
+module Scope
+  (T : sig
+    type key
+    type value
+    val create : key -> value
+  end) = struct
+
+  let scope = ref []
+
+  let is_empty () = !scope = []
+
+  (** adds a new scope with fresh vars *)
+  let push_scope vars =
+    let bindings = List.map (fun x -> (x, T.create x)) vars in
+    scope := bindings :: !scope
+
+  (** exits the outermost scope and forgets all bindings inside *)
+  let pop_scope () = begin
+      assert (not (is_empty ()));
+      scope := List.tl !scope
+    end
+
+  (** finds a symbol in any scope, including deeper ones.
+  If the symbol cannot be found, a new binding is created. *)
+  let find symbol =
+    let rec helper = function
+    | [] -> raise Not_found
+    | (x::_) when List.mem_assoc symbol x -> List.assoc symbol x
+    | (_::xs) -> helper xs in
+    try helper !scope
+    with Not_found -> begin
+      let v = T.create symbol in
+      scope := ( match !scope with
+        | [] -> [[symbol, v]]
+        | (hd::tl) -> ((symbol,v)::hd)::tl );
+      v
+    end
+
+end
+
+let const x _ = x;;
+
+(*s module to translate a basic tptp originated tree into a why AST tree *)
+module Translate = struct
+
+  (** an abstract type for the whole theory *)
+  let t =
+    let tv = Ty.create_tvsymbol (Ident.id_fresh "t") in
+    Ty.ty_var tv
+
+  module EnvVar = Scope(
+    struct
+      type key = variable
+      type value = Term.vsymbol
+      let create v = Term.create_vsymbol (id_fresh (String.uncapitalize v)) t
+    end)
+  module EnvFunctor = Scope(
+    struct
+      type key = (atom * Ty.ty list)
+      type value = Term.lsymbol
+      let create (v,l)  = Term.create_fsymbol (id_fresh (String.uncapitalize v)) l t
+    end)
+
+  (** translation for terms *)
+  let rec term2term = function
+  | TAtom x -> Term.t_app (EnvFunctor.find (x, [])) [] t
+  | TConst x -> Term.t_app (EnvFunctor.find (x, [])) [] t
+  | TVar x -> Term.t_var (EnvVar.find x)
+  | TFunctor (f, terms) ->
+      Term.t_app
+        (EnvFunctor.find (f, List.map (const t) terms))
+        (List.map term2term terms)
+        t
+
+  (** translation for formulae *)
+  let translate_binop = function | And -> Term.Fand | Or -> Term.For
+    | Implies -> Term.Fimplies | Equiv -> Term.Fiff
+  let translate_quant = function | Forall -> Term.Fforall | Exist -> Term.Fexists
+
+  let rec fmla2fmla = function
+  | FBinop (op, f1, f2) ->
+    Term.f_binary
+      (translate_binop op)
+      (fmla2fmla f1)
+      (fmla2fmla f2)
+  | FUnop (op, f) ->
+    assert (op = Not);
+    Term.f_not (fmla2fmla f)
+  | FQuant (quant, vars, f) -> begin
+    EnvVar.push_scope []; (* new scope *)
+    let answer = Term.f_quant
+      (translate_quant quant)
+      (List.map EnvVar.find vars)
+      [] (* no triggers *)
+      (fmla2fmla f) in
+    EnvVar.pop_scope (); (* exit scope *)
+    answer
+  end
+  | FPred (p, terms) ->
+    Term.f_app
+      (EnvFunctor.find (p, List.map (const t) terms))
+      (List.map term2term terms)
+  | FTermBinop (op, t1, t2) ->
+    Term.f_app
+      ( match op with
+        | Equal -> EnvFunctor.find ("=", [t;t])
+        | NotEqual -> EnvFunctor.find ("<>", [t;t]) )
+      [term2term t1; term2term t2]
+
+  let theory_of_decls theoryName decls = assert false;
+
+end
+
+let theory_of_decls = Translate.theory_of_decls

src/tptp2why/tptpTree.mli

-tptpTree.ml
\ No newline at end of file