tptp_ast.ml 2.58 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
Andrei Paskevich's avatar
Andrei Paskevich committed
11

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

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

type defined_type =
Andrei Paskevich's avatar
Andrei Paskevich committed
19 20
  | DTtype   | DTprop   | DTuniv   | DTint
  | DTrat    | DTreal   | DTdummy (* placeholder *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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
Andrei Paskevich's avatar
Andrei Paskevich committed
28

Andrei Paskevich's avatar
Andrei Paskevich committed
29 30 31
type defined_pred =
  | DPtrue   | DPfalse  | DPdistinct
  | DPless   | DPlesseq | DPgreater | DPgreatereq
Andrei Paskevich's avatar
Andrei Paskevich committed
32
  | DPisint  | DPisrat
Andrei Paskevich's avatar
Andrei Paskevich committed
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
Andrei Paskevich's avatar
Andrei Paskevich committed
38 39 40

(** Formula *)

Andrei Paskevich's avatar
Andrei Paskevich committed
41 42 43
type binop =
  | BOequ | BOnequ | BOimp  | BOpmi
  | BOand | BOor   | BOnand | BOnor
Andrei Paskevich's avatar
Andrei Paskevich committed
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
Andrei Paskevich's avatar
Andrei Paskevich committed
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
Andrei Paskevich's avatar
Andrei Paskevich committed
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)
Andrei Paskevich's avatar
Andrei Paskevich committed
74 75

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

(** Top level *)

type kind = TFF | FOF | CNF

type name = string
type file = string

type role =
88
  | Axiom | Hypothesis | Definition  | Assumption | Corollary
Andrei Paskevich's avatar
Andrei Paskevich committed
89
  | Lemma | Theorem    | Conjecture  | Negated_conjecture | Type
Andrei Paskevich's avatar
Andrei Paskevich committed
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
Andrei Paskevich's avatar
Andrei Paskevich committed
94

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