tptp_ast.ml 2.57 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

Andrei Paskevich's avatar
Andrei Paskevich committed
12
type loc = Why3.Loc.position
13 14 15

type atomic_word = string
type variable = string
Andrei Paskevich's avatar
Andrei Paskevich committed
16
type distinct = string
17 18

type defined_type =
Andrei Paskevich's avatar
Andrei Paskevich committed
19 20
  | DTtype   | DTprop   | DTuniv   | DTint
  | DTrat    | DTreal   | DTdummy (* placeholder *)
21

Andrei Paskevich's avatar
Andrei Paskevich committed
22 23 24 25 26 27
type defined_func =
  | DFumin   | DFsum    | DFdiff   | DFprod
  | DFquot   | DFquot_e | DFquot_t | DFquot_f
  | DFrem_e  | DFrem_t  | DFrem_f
  | DFfloor  | DFceil   | DFtrunc  | DFround
  | DFtoint  | DFtorat  | DFtoreal
28

Andrei Paskevich's avatar
Andrei Paskevich committed
29 30 31
type defined_pred =
  | DPtrue   | DPfalse  | DPdistinct
  | DPless   | DPlesseq | DPgreater | DPgreatereq
32
  | DPisint  | DPisrat
33

Andrei Paskevich's avatar
Andrei Paskevich committed
34 35 36 37
type defined_word =
  | DT of defined_type
  | DF of defined_func
  | DP of defined_pred
38 39 40

(** Formula *)

Andrei Paskevich's avatar
Andrei Paskevich committed
41 42 43
type binop =
  | BOequ | BOnequ | BOimp  | BOpmi
  | BOand | BOor   | BOnand | BOnor
44 45 46

type quant = Qforall | Qexists

Andrei Paskevich's avatar
Andrei Paskevich committed
47 48 49
type num_integer = string
type num_rational = string * string
type num_real = string * string option * string option
50 51

type number =
Andrei Paskevich's avatar
Andrei Paskevich committed
52 53
  | Nint  of num_integer
  | Nrat  of num_rational
Andrei Paskevich's avatar
Andrei Paskevich committed
54
  | Nreal of num_real
55

Andrei Paskevich's avatar
Andrei Paskevich committed
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
type expr = { e_node : expr_node ; e_loc : loc }

and expr_node =
  | Elet of expr * expr
  | Eite of expr * expr * expr
  | Eqnt of quant * tyvar list * expr
  | Ebin of binop * expr * expr
  | Enot of expr
  | Eequ of expr * expr
  | Eapp of atomic_word * expr list
  | Edef of defined_word * expr list
  | Evar of variable
  | Edob of distinct
  | Enum of number

and tyvar = variable * expr

type top_type = tyvar list * (expr list * expr)
74 75

type top_formula =
Andrei Paskevich's avatar
Andrei Paskevich committed
76
  | LogicFormula of expr
77
  | TypedAtom of atomic_word * top_type
Andrei Paskevich's avatar
Andrei Paskevich committed
78
  | Sequent of expr list * expr list
79 80 81 82 83 84 85 86 87 88

(** Top level *)

type kind = TFF | FOF | CNF

type name = string
type file = string

type role =
  | Axiom | Hypothesis | Definition  | Assumption
89
  | Lemma | Theorem    | Conjecture  | Negated_conjecture | Type
90 91 92

type input =
  | Formula of kind * name * role * top_formula * loc
Andrei Paskevich's avatar
Andrei Paskevich committed
93
  | Include of file * name list * loc
94

Andrei Paskevich's avatar
Andrei Paskevich committed
95
type tptp_file = input list
96