ptree.ml 3.9 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 33
type pp_binop =
  | 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
  | PPpor of pattern * pattern
Andrei Paskevich's avatar
Andrei Paskevich committed
60 61
  | PPpas of pattern * ident

62
type lexpr =
63 64 65
  { 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 * param 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
Andrei Paskevich's avatar
Andrei Paskevich committed
79
  | PPmatch of lexpr * (pattern * 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

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

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

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

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

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

134 135 136 137 138 139 140 141
type metarg =
  | PMAts  of qualid
  | PMAls  of qualid
  | PMApr  of qualid
  | PMAstr of string
  | PMAint of string

type decl =
142 143 144 145
  | TypeDecl of type_decl list
  | LogicDecl of logic_decl list
  | IndDecl of ind_decl list
  | PropDecl of loc * prop_kind * ident * lexpr
146
  | UseClone of loc * use * clone_subst list option
147
  | Meta of loc * ident * metarg list
148