tptpTranslate.ml 7.13 KB
Newer Older
1 2 3 4 5 6 7 8
(** 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

9 10 11 12 13 14 15 16 17
module S = Set.Make(String)
module M = Map.Make(String)

(** exploratory module, to find atoms and functors to be declared first *)
module Summary : sig
  type indic = Pred | Term
  val findAtoms : S.t -> fmla -> S.t
  val findFunctors : (indic * int) M.t ->
        TptpTree.fmla -> (indic * int) M.t
18
  val findAllAtoms : TptpTree.decl list -> S.t
19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
  val findAllFunctors : TptpTree.decl list -> (indic * int) M.t
end = struct
  type indic = Pred | Term

  let rec findAtoms_t s = function
  | TAtom a -> S.add a s
  | TConst _ | TVar _ -> s
  | TFunctor (_, terms) ->
    List.fold_left findAtoms_t s terms

  let rec findAtoms s = function
  | FBinop (_, f1, f2) -> S.union (findAtoms s f1) (findAtoms s f2)
  | FUnop (_, f) -> findAtoms s f
  | FQuant (_, _, f) -> findAtoms s f
  | FPred (_, terms) -> List.fold_left findAtoms_t s terms
  | FTermBinop (_, t1, t2) -> S.union (findAtoms_t s t1) (findAtoms_t s t2)

  let union_map = M.fold M.add

  let rec findFunctors_t m = function
  | TAtom _ | TConst _ | TVar _ -> m
  | TFunctor (f, terms) -> M.add f (Term, List.length terms) m

  let rec findFunctors m = function
  | FBinop (_, f1, f2) -> union_map (findFunctors m f1) (findFunctors m f2)
  | FUnop (_, f) -> findFunctors m f
  | FQuant (_, _, f) -> findFunctors m f
  | FPred (p, terms) -> let new_m = M.add p (Pred, List.length terms) m in
      List.fold_left findFunctors_t new_m terms
  | FTermBinop (_, t1, t2) ->
      union_map (findFunctors_t m t1) (findFunctors_t m t2)

  let findAllAtoms decls =
    let helper m = function Fof(_, _, f) -> findAtoms m f | _ -> assert false in
    List.fold_left helper S.empty decls

  let findAllFunctors decls =
    let helper s = function Fof(_, _, f) -> findFunctors s f | _ -> assert false in
    List.fold_left helper M.empty decls


end

62 63 64 65 66 67 68 69 70
(*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

71
  (* TODO : write a more efficient implementation, for example with maps *)
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102
  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

103 104
  let depth () = List.length !scope

105 106 107 108
end

let const x _ = x;;

109 110 111 112
let rec range n obj = match n with
| 0 -> []
| n -> obj::range (n-1) obj

113 114 115 116
(*s module to translate a basic tptp originated tree into a why AST tree *)
module Translate = struct

  (** an abstract type for the whole theory *)
117 118
  let ts = Ty.create_tysymbol (Ident.id_fresh "t") [] None
  let t = Ty.ty_app ts []
119

120
  (* TODO : replace it by a simple Map *)
121 122 123 124 125 126 127 128
  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
129
      type key = (atom * Ty.ty list * Summary.indic)
130
      type value = Term.lsymbol
131 132 133
      let create (v,l,ty) = match ty with
      | Summary.Term -> Term.create_fsymbol (id_fresh (String.uncapitalize v)) l t
      | Summary.Pred -> Term.create_psymbol (id_fresh (String.uncapitalize v)) l
134 135 136 137
    end)

  (** translation for terms *)
  let rec term2term = function
138 139
  | TAtom x -> Term.t_app (EnvFunctor.find (x, [], Summary.Term)) [] t
  | TConst x -> Term.t_app (EnvFunctor.find (x, [], Summary.Term)) [] t
140 141 142
  | TVar x -> Term.t_var (EnvVar.find x)
  | TFunctor (f, terms) ->
      Term.t_app
143
        (EnvFunctor.find (f, List.map (const t) terms, Summary.Term))
144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161
        (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
162 163
    (* Format.printf "@[<hov 2>quantifier %s %s (depth %d)@]\n" (if quant=Forall then "forall" else "exists") (String.concat ", " vars) (EnvVar.depth ()); *)
    EnvVar.push_scope vars; (* new scope *)
164 165 166 167 168 169 170 171 172 173
    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
174
      (EnvFunctor.find (p, List.map (const t) terms, Summary.Pred))
175 176 177
      (List.map term2term terms)
  | FTermBinop (op, t1, t2) ->
      ( match op with
178 179 180
        | Equal -> Term.f_equ_simp
        | NotEqual -> Term.f_neq_simp)
      (term2term t1) (term2term t2)
181

182 183 184 185 186 187 188 189
  let translatePropKind = function
  | Axiom -> Decl.Paxiom
  | Conjecture -> Decl.Pgoal

  (** add a declaration to a theory, after translation *)
  let addDecl theory = function
  | Fof(name, ty, f) ->
      let fmla = fmla2fmla f in
190
      (* print_endline ("adds declaration of "^name); *)
191 192 193 194 195
      Theory.add_prop_decl theory (translatePropKind ty)
        (Decl.create_prsymbol (id_fresh name)) fmla
  | Include _ -> assert false


196 197 198 199 200 201 202 203 204 205 206 207 208
  (** forward declaration of atoms and functors *)
  let addAtomForwardDecl name theory =
    (* Format.printf "declares %s\n (depth %d)" name (EnvVar.depth ()); *)
    let logic_decl = Decl.create_logic_decl
      [(EnvFunctor.find (name, [], Summary.Term)), None] in
    Theory.add_decl theory logic_decl

  let addFunctorsForwardDecl name obj theory =
    (* Format.printf "declares functor %s (type %s) (depth %d)\n" name (if fst obj = Summary.Pred then "pred" else "term"); *) 
    let logic_decl = Decl.create_logic_decl
      [(EnvFunctor.find (name, range (snd obj) t, (fst obj))), None] in
    Theory.add_decl theory logic_decl

209 210
  (** from a list of untyped declarations, translates them into a why theory *)
  let theory_of_decls theoryName decls =
211 212 213 214 215
    let theory = Theory.create_theory (Ident.id_fresh theoryName) in
    let theory = Theory.add_ty_decl theory [ts, Decl.Tabstract] in
    let theory = S.fold addAtomForwardDecl (Summary.findAllAtoms decls) theory in
    let theory = M.fold addFunctorsForwardDecl (Summary.findAllFunctors decls) theory in
    let theory = List.fold_left addDecl theory decls in
216
    Theory.close_theory theory
217 218 219 220

end

let theory_of_decls = Translate.theory_of_decls