plugins/tptp/tptp_ast.mli

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2024 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12 type loc = Why3.Loc.position
  13
  14 type atomic_word = string
  15 type variable = string
  16 type distinct = string
  17
  18 type defined_type =
  19   | DTtype   | DTprop   | DTuniv   | DTint
  20   | DTrat    | DTreal   | DTdummy (* placeholder *)
  21
  22 type defined_func =
  23   | DFumin   | DFsum    | DFdiff   | DFprod
  24   | DFquot   | DFquot_e | DFquot_t | DFquot_f
  25   | DFrem_e  | DFrem_t  | DFrem_f
  26   | DFfloor  | DFceil   | DFtrunc  | DFround
  27   | DFtoint  | DFtorat  | DFtoreal
  28
  29 type defined_pred =
  30   | DPtrue   | DPfalse  | DPdistinct
  31   | DPless   | DPlesseq | DPgreater | DPgreatereq
  32   | DPisint  | DPisrat
  33
  34 type defined_word =
  35   | DT of defined_type
  36   | DF of defined_func
  37   | DP of defined_pred
  38
  39 (** Formula *)
  40
  41 type binop =
  42   | BOequ | BOnequ | BOimp  | BOpmi
  43   | BOand | BOor   | BOnand | BOnor
  44
  45 type quant = Qforall | Qexists
  46
  47 type num_integer = string
  48 type num_rational = string * string
  49 type num_real = string * string option * string option
  50
  51 type number =
  52   | Nint  of num_integer
  53   | Nrat  of num_rational
  54   | Nreal of num_real
  55
  56 type expr = { e_node : expr_node ; e_loc : loc }
  57
  58 and expr_node =
  59   | Elet of expr * expr
  60   | Eite of expr * expr * expr
  61   | Eqnt of quant * tyvar list * expr
  62   | Ebin of binop * expr * expr
  63   | Enot of expr
  64   | Eequ of expr * expr
  65   | Eapp of atomic_word * expr list
  66   | Edef of defined_word * expr list
  67   | Evar of variable
  68   | Edob of distinct
  69   | Enum of number
  70
  71 and tyvar = variable * expr
  72
  73 type top_type = tyvar list * (expr list * expr)
  74
  75 type top_formula =
  76   | LogicFormula of expr
  77   | TypedAtom of atomic_word * top_type
  78   | Sequent of expr list * expr list
  79
  80 (** Top level *)
  81
  82 type kind = TFF | FOF | CNF
  83
  84 type name = string
  85 type file = string
  86
  87 type role =
  88   | Axiom | Hypothesis | Definition  | Assumption | Corollary
  89   | Lemma | Theorem    | Conjecture  | Negated_conjecture | Type
  90
  91 type input =
  92   | Formula of kind * name * role * top_formula * loc
  93   | Include of file * name list * loc
  94
  95 type tptp_file = input list
  96