ptree.ml 3.89 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

(*s Parse trees. *)

type loc = Loc.position

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
26 27
type real_constant = Term.real_constant
type constant = Term.constant
28

29 30 31
type pp_quant =
  | PPforall | PPexists

32
type pp_binop = 
33
  | PPand | PPor | PPimplies | PPiff 
34

35
type pp_unop = 
36
  | PPnot
37

38 39 40 41
type ident = { id : string; id_loc : loc }

type qualid =
  | Qident of ident
42
  | Qdot of qualid * ident
43

44 45 46
type pty =
  | PPTtyvar of ident
  | PPTtyapp of pty list * qualid
47
  | PPTtuple of pty list
48

49 50
type param = ident option * pty

Andrei Paskevich's avatar
Andrei Paskevich committed
51 52 53 54 55 56 57
type pattern =
  { pat_loc : loc; pat_desc : pat_desc }

and pat_desc =
  | PPpwild
  | PPpvar of ident
  | PPpapp of qualid * pattern list
58
  | PPptuple of pattern list
Andrei Paskevich's avatar
Andrei Paskevich committed
59 60
  | PPpas of pattern * ident

61 62 63 64
type lexpr = 
  { pp_loc : loc; pp_desc : pp_desc }

and pp_desc =
65 66
  | PPvar of qualid
  | PPapp of qualid * lexpr list
67 68 69
  | PPtrue
  | PPfalse
  | PPconst of constant
70 71 72
  | PPinfix of lexpr * ident * lexpr
  | PPbinop of lexpr * pp_binop * lexpr
  | PPunop of pp_unop * lexpr
73
  | PPif of lexpr * lexpr * lexpr
74
  | PPquant of pp_quant * param list * lexpr list list * lexpr
75
  | PPnamed of string * lexpr
76
  | PPlet of ident * lexpr * lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
77
  | PPeps of ident * pty * lexpr
78
  | PPmatch of lexpr list * (pattern list * lexpr) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
79
  | PPcast of lexpr * pty
80
  | PPtuple of lexpr list
81 82 83 84

(*s Declarations. *)

type plogic_type =
85
  | PPredicate of pty list
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
86
  | PFunction  of pty list * pty
87

88 89
type imp_exp =
  | Import | Export | Nothing
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
90

91
type use = {
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
92
  use_theory  : qualid;
93
  use_as      : ident option option;
94
  use_imp_exp : imp_exp;
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
95 96
}

97 98 99 100 101
type clone_subst =
  | CStsym  of qualid * qualid
  | CSlsym  of qualid * qualid
  | CSlemma of qualid
  | CSgoal  of qualid
102
      
103 104
type type_def = 
  | TDabstract
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
105
  | TDalias     of pty
106
  | TDalgebraic of (loc * ident * param list) list
107 108

type type_decl = {
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
109 110
  td_loc    : loc;
  td_ident  : ident;
111
  td_params : ident list;
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
112
  td_def    : type_def;
113 114 115
}

type logic_decl = { 
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
116 117
  ld_loc    : loc;
  ld_ident  : ident;
118
  ld_params : param list;
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
119 120
  ld_type   : pty option;
  ld_def    : lexpr option;
121 122
}

123 124 125
type ind_decl = {
  in_loc    : loc;
  in_ident  : ident;
126
  in_params : param list;
Andrei Paskevich's avatar
Andrei Paskevich committed
127
  in_def    : (loc * ident * lexpr) list;
128 129
}

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
130 131 132
type prop_kind =
  | Kaxiom | Klemma | Kgoal

133
type decl = 
134 135 136 137
  | TypeDecl of type_decl list
  | LogicDecl of logic_decl list
  | IndDecl of ind_decl list
  | PropDecl of loc * prop_kind * ident * lexpr
138
  | UseClone of loc * use * clone_subst list option
139
  | Namespace of loc * bool * ident option * decl list
140 141

type theory = {
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
142 143
  pt_loc  : loc;
  pt_name : ident;
144
  pt_decl : decl list;
145 146 147
}

type logic_file = theory list
148