Une nouvelle version du portail de gestion des comptes externes sera mise en production lundi 09 août. Elle permettra d'allonger la validité d'un compte externe jusqu'à 3 ans. Pour plus de détails sur cette version consulter : https://doc-si.inria.fr/x/FCeS

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
MARCHE Claude's avatar
MARCHE Claude committed
28
type label = Ident.label
29

30 31 32
type pp_quant =
  | PPforall | PPexists

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

36
type pp_unop =
37
  | PPnot
38

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

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

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

50 51
type param = ident option * pty

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

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

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

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

(*s Declarations. *)

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

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

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

99 100 101 102 103
type clone_subst =
  | CStsym  of qualid * qualid
  | CSlsym  of qualid * qualid
  | CSlemma of qualid
  | CSgoal  of qualid
104 105

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

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

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

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

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

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

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