blob: b6e04d3f2bfa0e6fa294f3e6f24e900b4a1b0c27 (
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
|
namespace Ast
open System
open System.Numerics
type Type =
| NamedType of string
| InstantiatedType of string * Type
type VarDecl =
| Var of string * Type option
type Expr =
| IntLiteral of BigInteger
| 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 VarDecl list * VarDecl list
type Member =
| Field of VarDecl
| Constructor of string * Signature * Expr * Expr
| Method of string * Signature * Expr * Expr
| Invariant of Expr list
type TopLevelDecl =
| Class of string * string list * Member list
| Model of string * string list * VarDecl list * Expr list * 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
|
