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

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

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

59 60 61
type uquant =
  ident list * pty

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

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

(*s Declarations. *)

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

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

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

98 99 100 101 102
type clone_subst =
  | CStsym  of qualid * qualid
  | CSlsym  of qualid * qualid
  | CSlemma of qualid
  | CSgoal  of qualid
103
      
104 105 106 107
type param = ident option * pty

type type_def = 
  | TDabstract
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
108
  | TDalias     of pty
109
  | TDalgebraic of (loc * ident * pty list) list
110 111

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

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

126 127 128 129
type ind_decl = {
  in_loc    : loc;
  in_ident  : ident;
  in_params : pty list;
Andrei Paskevich's avatar
Andrei Paskevich committed
130
  in_def    : (loc * ident * lexpr) list;
131 132
}

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
133 134 135
type prop_kind =
  | Kaxiom | Klemma | Kgoal

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

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

type logic_file = theory list
151