ptree.mli 3.63 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3 4 5 6 7
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
8 9 10 11 12 13 14 15 16 17 18
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41

(*s Parse trees. *)

type loc = Loc.position

(*s Logical expressions (for both terms and predicates) *)

type real_constant = 
  | RConstDecimal of string * string * string option (* int / frac / exp *)
  | RConstHexa of string * string * string

type constant =
  | ConstInt of string
  | ConstFloat of real_constant

type pp_infix = 
  PPand | PPor | PPimplies | PPiff |
  PPlt | PPle | PPgt | PPge | PPeq | PPneq |
  PPadd | PPsub | PPmul | PPdiv | PPmod

type pp_prefix = 
  PPneg | PPnot

42 43 44 45
type ident = { id : string; id_loc : loc }

type qualid =
  | Qident of ident
46
  | Qdot of qualid * ident
47

48 49 50
type pty =
  | PPTtyvar of ident
  | PPTtyapp of pty list * qualid
51 52 53 54 55

type lexpr = 
  { pp_loc : loc; pp_desc : pp_desc }

and pp_desc =
56 57
  | PPvar of qualid
  | PPapp of qualid * lexpr list
58 59 60 61 62 63
  | PPtrue
  | PPfalse
  | PPconst of constant
  | PPinfix of lexpr * pp_infix * lexpr
  | PPprefix of pp_prefix * lexpr
  | PPif of lexpr * lexpr * lexpr
64 65
  | PPforall of ident * pty * lexpr list list * lexpr
  | PPexists of ident * pty * lexpr
66
  | PPnamed of string * lexpr
67 68
  | PPlet of ident* lexpr * lexpr
  | PPmatch of lexpr * ((qualid * ident list * loc) * lexpr) list
69 70 71 72

(*s Declarations. *)

type plogic_type =
73 74
  | PPredicate of pty list
  | PFunction of pty list * pty
75

76 77
type imp_exp =
  | Import | Export | Nothing
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
78

79 80 81 82
type use = {
  use_theory : qualid;
  use_as : ident option;
  use_imp_exp : imp_exp;
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
83 84
}

85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
type param = ident option * pty

type type_def = 
  | TDabstract
  | TDalias of pty
  | TDalgebraic of (loc * ident * param list) list

type type_decl = {
  td_loc : loc;
  td_ident : ident;
  td_params : ident list;
  td_def : type_def;
}

type logic_decl = { 
  ld_loc : loc;
  ld_ident : ident;
  ld_params : param list;
  ld_type : pty option;
  ld_def : lexpr option;
}

type decl = 
  | TypeDecl of loc * type_decl list
  | Logic of loc * logic_decl list
110
  | Inductive_def of loc * ident * plogic_type * (loc * ident * lexpr) list
111 112
(*   | Function_def of loc * ident * (loc * ident * pty) list * pty * lexpr *)
(*   | Predicate_def of loc * ident * (loc * ident * pty) list * lexpr *)
113 114
  | Axiom of loc * ident * lexpr
  | Goal of loc * ident * lexpr
115
  | Use of loc * use
116
  | Namespace of loc * ident * decl list
117 118

type theory = {
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
119 120
  pt_loc  : loc;
  pt_name : ident;
121
  pt_decl : decl list;
122 123 124
}

type logic_file = theory list
125