blob: 5c42dbecfaa5ebf590877df37e1c3ce54fbce53a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
/// The AST of a Jennisy program
///
/// author: Rustan Leino (leino@microsoft.com)
/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
namespace Ast
open System
open System.Numerics
type Type =
| IntType
| BoolType
| SetType of Type (* type parameter *)
| SeqType of Type (* type parameter *)
| NamedType of string * string list (* type parameters *)
| InstantiatedType of string * Type list (* type parameters *)
type VarDecl =
| Var of string * Type option
type Expr =
| IntLiteral of int
| IdLiteral of string
| Star
| Dot of Expr * string
| UnaryExpr of string * Expr
| BinaryExpr of int * string * Expr * Expr
| SelectExpr of Expr * Expr
| UpdateExpr of Expr * Expr * Expr
| SequenceExpr of Expr list
| SeqLength of Expr
| ForallExpr of VarDecl list * Expr
type Stmt =
| Block of Stmt list
| Assign of Expr * Expr
type Signature =
| Sig of (* ins *) VarDecl list * (* outs *) VarDecl list
type Member =
| Field of VarDecl
| Method of (* name *) string * Signature * (* pre *) Expr * (* post *) Expr * (* isConstructor *) bool
| Invariant of Expr list
type TopLevelDecl =
| Class of string * string list * Member list
| Model of string * string list * VarDecl list * (* frame *) Expr list * (* invariant *) Expr
| Code of string * string list
type SyntacticProgram =
| SProgram of TopLevelDecl list
type Component =
| Component of (*class*)TopLevelDecl * (*model*)TopLevelDecl * (*code*)TopLevelDecl
type Program =
| Program of Component list
type Const =
| IntConst of int
| BoolConst of bool
| SetConst of Set<Const>
| SeqConst of Const list
| NullConst
| NoneConst
| ThisConst of (* loc id *) string * Type option
| NewObj of (* loc id *) string * Type option
| ExprConst of Expr
| VarConst of (* varName *) string
| Unresolved of (* loc id *) string
|
