ocarina-me_real-real_tree-nodes.idl 5.07 KB
Newer Older
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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
// REAL Tree

module Ocarina::ME_REAL::REAL_Tree::Nodes {

  /******************/
  /* Internal types */
  /******************/

  typedef long  Name_Id;
  typedef long  Value_Id;
  typedef octet Operator_Id;

  /******************/
  /* Internal nodes */
  /******************/

  interface Node_Id {
    Node_Id  Next_Node;        // Link nodes together
  };

  interface Identifier : Node_Id {
    Name_Id   Name;
  };

  interface List_Id {
    Node_Id  First_Node;
    Node_Id  Last_Node;
  }; 

  interface Node_Container : Node_Id {
    Node_Id  Item;
  };

  /**********************/
  /* Set-relative nodes */
  /**********************/

  //  Element of a set
  interface Element : Node_Id { 
    Node_Id   Identifier;
    Value_Id  Element_Type;
    Node_Id   Set_Reference;    //  reference on (unique) owner set 
  };

  interface Set : Node_Id {
    Node_Id    Identifier;
    Value_Id   Set_Type;
    Node_Id    Annotation;
    Node_Id    Set_Expression;
    Value_Id   Predefined_Type;
    Value_Id   Dependant;
  };

  interface Set_Reference : Identifier {
    Node_Id    Referenced_Set;     //  an existing set
    Value_Id   Predefined_Type;
  };

 interface Value_Node : Node_Id {
    Value_Id Item_Val;
  };
    
  /******************/
  /* Language nodes */
  /******************/

  interface Variable : Node_Id {
    Node_Id    Identifier;
    Value_Id   Var_Value;
    Value_Id   Var_Type;
  };

  interface Theorem_Reference : Node_Id {
    Name_Id   Theorem_Name;
    Node_Id   Related_Theorem;
  };

  interface Var_Reference : Identifier {
    Node_Id    Referenced_Var;  //  an existing variable
    Value_Id   Returned_Type;
  };

  interface Variable_Declaration : Node_Id {
    Node_Id    Var_Ref;    //  var_reference
    Value_Id   Is_Global;  //  0 => false, 1 => true
  };

  interface Variable_Decl_Compute : Theorem_Reference {
    Node_Id    Var_Ref;     //  var_reference
    List_Id    True_params; //  (opt) sub-theorem arguments
    Node_Id    Domain;      //  (opt) set or node_id
    List_Id    Parameters;  //  (opt) list of value_id
    Value_Id   Is_Global;   //  0 => false, 1 => true
  };

  interface Variable_Decl_Expression : Variable_Declaration {
    Node_Id    Return_Expr;  //  Return expression
  };

  interface Literal : Node_Id {
    Value_Id    Value;
    Value_Id    Returned_Type;
  };

  interface Parametrized_Identifier : Node_Id {
    Node_Id     Identifier;
    Value_Id    Code;
    List_Id     Parameters;  // Literal, Set, Element, Variable or expression
  };

  interface Expression : Node_Id {
    Node_Id     Right_Expr;  //  either an Expression, *_Expression, Set_Reference,
    Node_Id     Left_Expr;   //  Selection_Subprogram_Call, Check_Subprogram_Call, 
                             //  or a litteral
    Operator_Id Operator;
  };

  //  after 'in'
  // sub-expressions are either Set_Expressions or Set_References
  interface Set_Expression : Expression {
    Value_Id  Set_Type;  //  expression return type
  };

  interface Check_Subprogram_Call : Parametrized_Identifier {
    List_Id   Referenced_Sets;
    List_Id   True_Parameters;
    Value_Id  Variable_Position; 
    //  Only for selection subprograms
    //  tells whether the variable is the first argument (value 1)
    //  or the second one (value 2)
    //  initial value is 0

    Value_Id  Returned_Type;
  };

  //  After 'check' and between parenthesis
  interface Check_Expression : Expression {
    Value_Id  Returned_Type;
  };

  interface Ternary_Expression : Check_Expression {
    Node_Id   Third_Expr;
  };

  interface Return_Expression : Node_Id {
    Node_Id   Check_Expression;
    Value_Id  Range_Function;  // function to be applied to the resulting set
  };

  interface Range_Declaration : Node_Id {
    Node_Id   Variable_Ref;   //  Var_Reference
    Node_Id   Range_Variable; //  Element
    Node_Id   Range_Set;      //  Set_Expression
  };

  interface Local_Variable_Definition : Element {
    Node_Id   In_Set;  //  Set_Expression or Set_Reference
  };

  interface Set_Declaration : Set_Reference {
    Node_Id   Parametrized_Expr;
    Node_Id   Corresponding_Element;
    Node_Id   Selection_Expression;
    Node_Id   Local_Variable;  //  Var_Reference
    Node_Id   Local_Set;       //  Set_Reference
    Node_Id   Local_Set_Expression;
    Value_Id  Dependant;       // the set refers to the global range variable
  };

  interface Required_Theorem : Theorem_Reference {
  };

  interface Theorem : Node_Id {
    Node_Id   Identifier;
    Node_Id   Range_Declaration;
    List_Id   Declarations;      //  sets and variables declarations
    List_Id   Required_Theorems;
    Node_Id   Check_Expression;
    Node_Id   Return_Expression;
    List_Id   Used_Set;          //  actual set declaration (Set)
    List_Id   Used_Var;          //  list of globally-visible variables
    List_Id   Local_Var;         //  list of local variables
    Node_Id   Related_Entity;    //  corresponding AADL entity
  };

  interface Root_Node : Node_Id {
    List_Id   Theorems;
  };

  /**********************/
  /*   Annotation node  */
  /**********************/

  interface Annotation : Node_Id {
    Value_Id  Index;
  };
};