1
------------------------------------------------------------------------------
2
--                                                                          --
3
--                           OCARINA COMPONENTS                             --
4
--                                                                          --
5
--               O C A R I N A . F E _ R E A L . P A R S E R                --
6
--                                                                          --
7
--                                 B o d y                                  --
8
--                                                                          --
9
--                  Copyright (C) 2009 Telecom ParisTech,                   --
10
--                 2010-2019 ESA & ISAE, 2019-2020 OpenAADL                 --
11
--                                                                          --
12
-- Ocarina  is free software; you can redistribute it and/or modify under   --
13
-- terms of the  GNU General Public License as published  by the Free Soft- --
14
-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
15
-- sion. Ocarina is distributed in the hope that it will be useful, but     --
16
-- WITHOUT ANY WARRANTY; without even the implied warranty of               --
17
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                     --
18
--                                                                          --
19
-- As a special exception under Section 7 of GPL version 3, you are granted --
20
-- additional permissions described in the GCC Runtime Library Exception,   --
21
-- version 3.1, as published by the Free Software Foundation.               --
22
--                                                                          --
23
-- You should have received a copy of the GNU General Public License and    --
24
-- a copy of the GCC Runtime Library Exception along with this program;     --
25
-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
26
-- <http://www.gnu.org/licenses/>.                                          --
27
--                                                                          --
28
--                    Ocarina is maintained by OpenAADL team                --
29
--                              (info@openaadl.org)                         --
30
--                                                                          --
31
------------------------------------------------------------------------------
32

33
with Ocarina.FE_REAL.Lexer;
34
with Ocarina.FE_REAL.Parser_Errors;
35
with Ocarina.ME_REAL.Tokens;
36
with Ocarina.ME_REAL.REAL_Tree.Nodes;
37
with Ocarina.ME_REAL.REAL_Tree.Utils;
38
with Ocarina.ME_REAL.REAL_Tree.Nutils;
39
with Ocarina.REAL_Values;
40
with Ocarina.Builder.REAL;
41
with Ocarina.Parser;
42
with Ocarina.Files;
43
with Ocarina.Analyzer.REAL;
44
with Ocarina.Namet;
45

46 1
package body Ocarina.FE_REAL.Parser is
47

48
   use Ocarina.ME_REAL.REAL_Tree.Nodes;
49
   use Ocarina.ME_REAL.REAL_Tree.Utils;
50
   use Ocarina.ME_REAL.REAL_Tree.Nutils;
51
   use Ocarina.ME_REAL.Tokens;
52
   use Ocarina.Analyzer.REAL;
53
   use Ocarina.Builder.REAL;
54
   use Ocarina.FE_REAL.Lexer;
55
   use Ocarina.FE_REAL.Parser_Errors;
56

57
   function P_Theorem return Node_Id;
58

59
   function P_Set_Range_Declaration return Node_Id;
60

61
   procedure P_Declarations (R : Node_Id; Success : out Boolean);
62
   --  Parse sets and variables declarations
63

64
   function Create_Check_Expression return Node_Id;
65

66
   function P_Check_Expression return Node_Id;
67
   --  FIXME :
68
   --  Bug with 'true' and 'false' boolean literals which
69
   --  cannot be parsed yet, cause unknown.
70

71
   function P_Set_Expression return Node_Id;
72
   function P_Higher_Level_Function return Value_Id;
73
   function P_Single_Set_Declaration return Node_Id;
74
   function P_Create_Set_Identifier return Node_Id;
75
   function P_Check_Subprogram_Call return Node_Id;
76
   function P_Ternary_Expression return Node_Id;
77
   function P_Expression return Node_Id;
78

79
   function P_Requirements return List_Id;
80
   --  Get required theorems.
81
   --  Does *not* check for existence (cf. analyzer)
82

83
   function P_Identifier return Node_Id;
84
   function Make_Literal (T : Token_Type) return Node_Id;
85

86
   procedure Skip_To_Theorem_End (Success : out Boolean);
87
   --  Whenever an error occurs in parsing, this procedure will
88
   --  search for the nearest 'end;' keywords, in order to avoid
89
   --  parsing errors to spread to the following theorems.
90

91 1
   Current_Theorem_Node : Node_Id;
92
   Current_Theorem_Name : Name_Id;
93

94
   package Expressions is new GNAT.Table (Node_Id, Natural, 1, 100, 10);
95

96
   Preferences : constant array (OV_Equal .. OV_Power) of Natural :=
97
     (OV_Power         => 1,
98
      OV_Not           => 2,
99
      OV_Star          => 3,
100
      OV_Slash         => 4,
101
      OV_Modulo        => 5,
102
      OV_Minus         => 6,
103
      OV_Plus          => 7,
104
      OV_Greater       => 8,
105
      OV_Less          => 9,
106
      OV_Greater_Equal => 10,
107
      OV_Less_Equal    => 11,
108
      OV_Different     => 12,
109
      OV_Equal         => 13,
110
      OV_Or            => 14,
111
      OV_And           => 15);
112

113
   ----------------------
114
   -- P_Set_Expression --
115
   ----------------------
116

117 1
   function P_Set_Expression return Node_Id is
118
      use Expressions;
119

120
      function Is_Expression_Completed return Boolean;
121
      --  Return True when there are no more token to read to complete
122
      --  the current expression.
123

124
      function P_Expression_Part return Node_Id;
125
      --  Return a node describing an expression. It is either a
126
      --  binary operator (an operator with no right expression
127
      --  assigned) or an expression value (a scoped name, a literal
128
      --  or an expression with an unary operator - that is a binary
129
      --  operator with a right inner expression and no left inner
130
      --  expression - or an expression with both inner expressions
131
      --  assigned). Note that whether an operator is a binary or
132
      --  unary operator is resolved in this routine. For a unary
133
      --  operator, we check that the previous token was a binary
134
      --  operator.
135

136
      function Is_Binary_Operator (E : Node_Id) return Boolean;
137
      --  Return True when N is an operator with the right expression
138
      --  *still* not assigned. Otherwise, an operator with a right
139
      --  expression is a value expression.
140

141
      function Is_Expression_Value (E : Node_Id) return Boolean;
142
      --  Return True when N is not an operator (literal or scoped
143
      --  name) or else when its right expression is assigned (unary
144
      --  operator).
145

146
      function Precede (L, R : Node_Id) return Boolean;
147
      --  Does operator L precedes operator R
148

149
      function Translate_Operator (T : Token_Type) return Operator_Id;
150
      --  Return the Operator_Id corresponding to the token read
151

152
      ------------------------
153
      -- Translate_Operator --
154
      ------------------------
155

156 1
      function Translate_Operator (T : Token_Type) return Operator_Id is
157
      begin
158
         case T is
159 0
            when T_Star =>
160 0
               return OV_Star;
161

162 0
            when T_Plus =>
163 0
               return OV_Plus;
164

165 1
            when T_Minus =>
166 1
               return OV_Minus;
167

168 0
            when others =>
169 0
               return OV_Invalid;
170
         end case;
171
      end Translate_Operator;
172

173
      -----------------------------
174
      -- Is_Expression_Completed --
175
      -----------------------------
176

177 1
      function Is_Expression_Completed return Boolean is
178 1
         T : constant Token_Type := Next_Token;
179
      begin
180 1
         return T /= T_Identifier
181 1
           and then T not in Predefined_Sets
182 1
           and then T /= T_Left_Paren
183 1
           and then not Is_Set_Operator (T);
184
      end Is_Expression_Completed;
185

186
      -------------------------
187
      -- Is_Expression_Value --
188
      -------------------------
189

190 0
      function Is_Expression_Value (E : Node_Id) return Boolean is
191
      begin
192 0
         return Kind (E) = K_Set
193 0
           or else
194 0
           (Kind (E) = K_Set_Expression and then Present (Right_Expr (E)));
195
      end Is_Expression_Value;
196

197
      ------------------------
198
      -- Is_Binary_Operator --
199
      ------------------------
200

201 1
      function Is_Binary_Operator (E : Node_Id) return Boolean is
202
      begin
203 1
         return Kind (E) = K_Set_Expression
204
           and then Operator (E) in Operator_Values
205 1
           and then No (Right_Expr (E));
206
      end Is_Binary_Operator;
207

208
      -----------------------
209
      -- P_Expression_Part --
210
      -----------------------
211

212 1
      function P_Expression_Part return Node_Id is
213 1
         Expression     : Node_Id;
214 1
         Previous_Token : Token_Type;
215 1
         Op             : Operator_Id;
216
      begin
217
         case Next_Token is
218

219 1
            when T_Identifier =>
220

221
               --  We build a set reference with identifier name
222 1
               Scan_Token;
223 1
               Expression := New_Node (K_Set_Reference, Token_Location);
224 1
               Set_Name (Expression, To_Lower (Token_Name));
225 1
               Set_Predefined_Type (Expression, SV_No_Type);
226 1
               Set_Referenced_Set (Expression, No_Node);
227

228 1
            when T_Processor_Set .. T_Local_Set =>
229

230
               --  We build a set reference with predefined name
231 1
               Scan_Token;
232 1
               Expression := New_Node (K_Set_Reference, Token_Location);
233 1
               Set_Name (Expression, To_Lower (Token_Name));
234 1
               Set_Predefined_Type
235
                 (Expression,
236 1
                  Translate_Predefined_Sets (Token));
237 1
               Set_Referenced_Set (Expression, No_Node);
238

239 1
            when T_Left_Paren =>
240

241
               --  Look for a parenthesized expression value
242

243
               --  past '(', no error possible
244

245 1
               Scan_Token (T_Left_Paren);
246

247 1
               Expression := P_Set_Expression;
248

249 1
               Scan_Token (T_Right_Paren);
250 1
               if Token = T_Error then
251 0
                  DPE (PC_Set_Expression, T_Right_Paren);
252 0
                  return No_Node;
253
               end if;
254

255 1
            when T_Plus | T_Minus | T_Star =>
256

257
               --  Look for a binary/unary operator
258

259 1
               Previous_Token := Token;
260 1
               Scan_Token;  --  past binary/unary operator
261

262 1
               Expression := New_Node (K_Set_Expression, Token_Location);
263 1
               Set_Set_Type (Expression, SV_No_Type);
264

265 1
               Op := Translate_Operator (Token);
266 1
               if Op = OV_Invalid then
267 0
                  DPE (PC_Set_Expression, EMC_Expected_Valid_Operator);
268 0
                  Set_Last (First - 1);
269 0
                  return No_Node;
270
               end if;
271 1
               Set_Operator (Expression, Op);
272

273
               --  Cannot have two following operators except in the
274
               --  special case above.
275

276 1
               if Is_Operator (Previous_Token) then
277 0
                  DPE (PC_Set_Expression, EMC_Expected_Valid_Operator);
278 0
                  return No_Node;
279
               end if;
280

281 0
            when others =>
282 0
               DPE (PC_Set_Expression, EMC_Cannot_Parse_Set_Expression);
283 0
               return No_Node;
284 1
         end case;
285

286 1
         return Expression;
287
      end P_Expression_Part;
288

289
      -------------
290
      -- Precede --
291
      -------------
292

293 0
      function Precede (L, R : Node_Id) return Boolean is
294 0
         Left_Operator  : constant Operator_Id := Operator (L);
295 0
         Right_Operator : constant Operator_Id := Operator (R);
296
      begin
297 0
         return Preferences (Left_Operator) < Preferences (Right_Operator);
298
      end Precede;
299

300 1
      Expr  : Node_Id;
301 1
      First : Natural;
302
   begin
303

304
      --  Read enough expressions to push as first expression a binary
305
      --  operator with no right expression
306

307 1
      Expr := P_Expression_Part;
308 1
      if No (Expr) then
309 0
         return No_Node;
310
      end if;
311

312
      --  We must have first an expression value
313

314 1
      if Is_Binary_Operator (Expr) then
315 0
         DPE (PC_Set_Expression, EMC_Cannot_Parse_Set_Expression);
316 0
         return No_Node;
317
      end if;
318

319
      --  We have only one expression value
320

321 1
      if Is_Expression_Completed then
322 1
         return Expr;
323
      end if;
324

325 1
      Increment_Last;
326
      Table (Last) := Expr;
327 1
      First        := Last;
328

329 1
      Expr := P_Expression_Part;
330 1
      if No (Expr) then
331 0
         Set_Last (First - 1);
332 0
         return No_Node;
333
      end if;
334

335
      --  We must have a binary operator as the first expression is an
336
      --  expression value.
337

338 1
      if not Is_Binary_Operator (Expr) then
339 0
         DPE (PC_Set_Expression, EMC_Cannot_Parse_Set_Expression);
340 0
         Set_Last (First - 1);
341 0
         return No_Node;
342
      end if;
343

344
      Set_Left_Expr (Expr, Table (Last));
345
      Table (Last) := Expr;
346

347
      --  Push expressions in stack and check that the top of the
348
      --  stack consists in one or more binary operators with no
349
      --  right expr and zero or one expression value.
350

351 1
      while not Is_Expression_Completed loop
352

353 1
         Expr := P_Expression_Part;
354 1
         if No (Expr) then
355 0
            return No_Node;
356
         end if;
357

358 1
         Increment_Last;
359
         Table (Last) := Expr;
360

361
         --  Check that this new expression is not a binary operator
362
         --  when the previous one is a binary operator with no right
363
         --  expression.
364

365 1
         if First < Last
366 1
           and then Is_Binary_Operator (Expr)
367 0
           and then No (Left_Expr (Expr))
368 0
           and then Is_Binary_Operator (Table (Last - 1))
369
         then
370 0
            DPE (PC_Set_Expression, EMC_Cannot_Parse_Set_Expression);
371 0
            Set_Last (First - 1);
372 0
            return No_Node;
373
         end if;
374

375
         --  Check whether we have a sequence of a binary operator
376
         --  (left operator), an expression value and another binary
377
         --  operator (right operator). In this case, if the left
378
         --  operator has a better precedence than the right one, we
379
         --  can reduce the global expression by assigning the
380
         --  expression value to the right expression of the left
381
         --  operator. Then as the left operator has already a left
382
         --  expression, it becomes an expression value which can be
383
         --  assign to the left expression of the right operation.
384
         --  Recompute the size of the expression stack.
385

386
         while First + 1 < Last
387 0
           and then Is_Expression_Value (Table (Last - 1))
388 0
           and then Precede (Table (Last - 2), Expr)
389
         loop
390 0
            Set_Right_Expr (Table (Last - 2), Table (Last - 1));
391 0
            Set_Left_Expr (Table (Last), Table (Last - 2));
392 0
            Table (Last - 2) := Table (Last);
393 0
            Set_Last (Last - 2);
394 0
         end loop;
395 1
      end loop;
396

397
      --  The last expression is not a value. We cannot reduce the
398
      --  global expression
399

400
      if Is_Binary_Operator (Table (Last)) then
401 0
         DPE (PC_Set_Expression, EMC_Cannot_Parse_Set_Expression);
402 0
         Set_Last (First - 1);
403 0
         return No_Node;
404
      end if;
405

406
      --  Reduce the global expression
407

408 1
      while First < Last loop
409
         if No (Left_Expr (Table (Last - 1))) then
410 0
            Set_Right_Expr (Table (Last - 1), Table (Last));
411 0
            Set_Left_Expr (Table (Last - 1), Table (Last - 2));
412 0
            Table (Last - 2) := Table (Last - 1);
413 0
            Set_Last (Last - 2);
414

415
         else
416
            Set_Right_Expr (Table (Last - 1), Table (Last));
417
            Set_Last (Last - 1);
418
         end if;
419 1
      end loop;
420

421
      Expr := Table (First);
422
      Set_Last (First - 1);
423

424 1
      return Expr;
425

426
   end P_Set_Expression;
427

428
   ------------------------
429
   -- P_Check_Expression --
430
   ------------------------
431

432 1
   function P_Check_Expression return Node_Id is
433
      use Expressions;
434

435
      function Is_Expression_Completed return Boolean;
436
      --  Return True when there are no more token to read to complete
437
      --  the current expression.
438

439
      function P_Expression_Part return Node_Id;
440
      --  Return a node describing an expression. It is either a
441
      --  binary operator (an operator with no right expression
442
      --  assigned) or an expression value (a scoped name, a literal
443
      --  or an expression with an unary operator - that is a binary
444
      --  operator with a right inner expression and no left inner
445
      --  expression - or an expression with both inner expressions
446
      --  assigned). Note that whether an operator is a binary or
447
      --  unary operator is resolved in this routine. For a unary
448
      --  operator, we check that the previous token was a binary
449
      --  operator.
450

451
      function Is_Binary_Operator (E : Node_Id) return Boolean;
452
      --  Return True when N is an operator with the right expression
453
      --  *still* not assigned. Otherwise, an operator with a right
454
      --  expression is a value expression.
455

456
      function Is_Expression_Value (E : Node_Id) return Boolean;
457
      --  Return True when N is not an operator (literal or scoped
458
      --  name) or else when its right expression is assigned (unary
459
      --  operator).
460

461
      function Precede (L, R : Node_Id) return Boolean;
462
      --  Does operator L precedes operator R
463

464
      function Translate_Operator (T : Token_Type) return Operator_Id;
465
      --  Return the operator corresponding to the parameter-given token
466

467
      ------------------------
468
      -- Translate_Operator --
469
      ------------------------
470

471 1
      function Translate_Operator (T : Token_Type) return Operator_Id is
472
      begin
473
         case T is
474 1
            when T_Or =>
475 1
               return OV_Or;
476

477 1
            when T_And =>
478 1
               return OV_And;
479

480 1
            when T_Not =>
481 1
               return OV_Not;
482

483 1
            when T_Equal =>
484 1
               return OV_Equal;
485

486 1
            when T_Different =>
487 1
               return OV_Different;
488

489 1
            when T_Greater =>
490 1
               return OV_Greater;
491

492 1
            when T_Less =>
493 1
               return OV_Less;
494

495 1
            when T_Greater_Equal =>
496 1
               return OV_Greater_Equal;
497

498 1
            when T_Less_Equal =>
499 1
               return OV_Less_Equal;
500

501 1
            when T_Minus =>
502 1
               return OV_Minus;
503

504 1
            when T_Plus =>
505 1
               return OV_Plus;
506

507 1
            when T_Modulo =>
508 1
               return OV_Modulo;
509

510 1
            when T_Star =>
511 1
               return OV_Star;
512

513 1
            when T_Slash =>
514 1
               return OV_Slash;
515

516 1
            when T_Power =>
517 1
               return OV_Power;
518

519 0
            when others =>
520 0
               return OV_Invalid;
521
         end case;
522
      end Translate_Operator;
523

524
      -----------------------------
525
      -- Is_Expression_Completed --
526
      -----------------------------
527

528 1
      function Is_Expression_Completed return Boolean is
529 1
         T : constant Token_Type := Next_Token;
530
      begin
531 1
         return T not in Literal_Type
532 1
           and then T /= T_Identifier
533 1
           and then T not in Selection_Function_Type
534 1
           and then T not in Verification_Function_Type
535 1
           and then T /= T_Left_Paren
536 1
           and then T not in T_Equal .. T_Power;
537
      end Is_Expression_Completed;
538

539
      -------------------------
540
      -- Is_Expression_Value --
541
      -------------------------
542

543 1
      function Is_Expression_Value (E : Node_Id) return Boolean is
544
      begin
545 1
         return Kind (E) = K_Literal
546 1
           or else Kind (E) = K_Identifier
547 1
           or else Kind (E) = K_Var_Reference
548
           or else
549
           (Operator (E) not in OV_Equal .. OV_Power
550 0
            and then Operator (E) /= OV_Equal)
551 1
           or else Present (Right_Expr (E));
552
      end Is_Expression_Value;
553

554
      ------------------------
555
      -- Is_Binary_Operator --
556
      ------------------------
557

558 1
      function Is_Binary_Operator (E : Node_Id) return Boolean is
559
      begin
560 1
         return Kind (E) = K_Check_Expression
561
           and then Operator (E) in OV_Equal .. OV_Power
562 1
           and then No (Right_Expr (E));
563
      end Is_Binary_Operator;
564

565
      -----------------------
566
      -- P_Expression_Part --
567
      -----------------------
568

569 1
      function P_Expression_Part return Node_Id is
570 1
         Expression     : Node_Id;
571 1
         Right_Expr     : Node_Id;
572 1
         Previous_Token : Token_Type;
573 1
         Op             : Operator_Id;
574
      begin
575
         case Next_Token is
576

577 1
            when T_Is_Subcomponent_Of .. T_Is_Connecting_To =>
578

579
               --  We build a check (in this case, verification)
580
               --  subprogram call
581

582 1
               Expression := P_Check_Subprogram_Call;
583 1
               if No (Expression) then
584 0
                  return No_Node;
585
               end if;
586

587 1
            when T_Get_Property_Value .. T_Sum =>
588

589
               --  We build a check subprogram call
590

591 1
               Expression := P_Check_Subprogram_Call;
592 1
               if No (Expression) then
593 0
                  return No_Node;
594
               end if;
595

596 1
            when T_Left_Paren =>
597

598
               --  Look for a parenthesized expression value
599

600 1
               Scan_Token;  --  past '('
601 1
               Expression := P_Expression;
602 1
               Scan_Token (T_Right_Paren);
603 1
               if Token = T_Error then
604 0
                  DPE (PC_Check_Expression, T_Right_Paren);
605 0
                  return No_Node;
606
               end if;
607

608 1
            when T_Equal .. T_Power =>
609

610
               --  Look for a binary/unary operator
611

612 1
               Previous_Token := Token;
613 1
               Scan_Token;  --  past binary/unary operator
614 1
               Expression := New_Node (K_Check_Expression, Token_Location);
615

616 1
               Op := Translate_Operator (Token);
617 1
               if Op = OV_Invalid then
618 0
                  DPE (PC_Check_Expression, EMC_Expected_Valid_Operator);
619 0
                  Set_Last (First - 1);
620 0
                  return No_Node;
621
               end if;
622 1
               Set_Operator (Expression, Op);
623

624
               --  Token is a real unary operator
625

626 1
               if Token = T_Not
627
                 or else
628 1
                 (Token = T_Minus
629 1
                  and then Previous_Token /= T_Affect
630 1
                  and then Previous_Token /= T_Right_Paren
631
                  and then
632 1
                  (Is_Operator (Previous_Token)
633 1
                   or else Previous_Token = T_Left_Paren))
634
               then
635
                  case Next_Token is
636 1
                     when T_Get_Property_Value .. T_Sum |
637
                       T_Left_Paren                     |
638
                       T_Identifier                     =>
639

640 1
                        Right_Expr := P_Expression;
641 1
                        if No (Right_Expr) then
642 0
                           return No_Node;
643
                        end if;
644 1
                        Set_Right_Expr (Expression, Right_Expr);
645

646 0
                     when others =>
647 0
                        DPE (PC_Check_Expression, EMC_Expected_Valid_Operator);
648 0
                        return No_Node;
649 1
                  end case;
650

651
               --  Cannot have two following operators except in the
652
               --  special case above.
653

654 1
               elsif Is_Operator (Previous_Token) then
655 0
                  DPE (PC_Check_Expression, EMC_Unexpected_Operator);
656 0
                  return No_Node;
657
               end if;
658

659 1
            when T_False .. T_Wide_String_Literal =>
660

661
               --  Look for a literal
662

663 1
               Scan_Token;
664 1
               Expression := Make_Literal (Token);
665

666 1
            when T_Identifier =>
667

668
               --  The only identifier allowed are variables names
669

670 1
               Expression := P_Identifier;
671 1
               Expression := Make_Var_Reference (Name (Expression));
672

673 0
            when others =>
674 0
               DPE (PC_Check_Expression, EMC_Cannot_Parse_Check_Expression);
675 0
               return No_Node;
676 1
         end case;
677

678 1
         return Expression;
679
      end P_Expression_Part;
680

681
      -------------
682
      -- Precede --
683
      -------------
684

685 1
      function Precede (L, R : Node_Id) return Boolean is
686 1
         Left_Operator : constant Operator_Id := Operator (L);
687
--         Right_Operator : constant Operator_Id := Operator (R);
688
      begin
689 1
         if Kind (R) = K_Check_Subprogram_Call then
690 0
            return True;
691
         end if;
692

693
         return Preferences (Left_Operator) < Preferences (Operator (R));
694
      end Precede;
695

696 1
      Expr  : Node_Id;
697 1
      First : Natural;
698
   begin
699

700
      --  Read enough expressions to push as first expression a binary
701
      --  operator with no right expression
702

703 1
      Expr := P_Expression_Part;
704 1
      if No (Expr) then
705 0
         return No_Node;
706
      end if;
707

708
      --  We must have first an expression value
709

710 1
      if Is_Binary_Operator (Expr) then
711 0
         DPE (PC_Check_Expression, EMC_Cannot_Parse_Check_Expression);
712 0
         return No_Node;
713
      end if;
714

715
      --  We have only one expression value
716

717 1
      if Is_Expression_Completed then
718 1
         return Expr;
719
      end if;
720

721 1
      Increment_Last;
722
      Table (Last) := Expr;
723 1
      First        := Last;
724

725 1
      Expr := P_Expression_Part;
726 1
      if No (Expr) then
727 0
         Set_Last (First - 1);
728 0
         return No_Node;
729
      end if;
730

731
      --  We must have a binary operator as the first expression is an
732
      --  expression value.
733

734 1
      if not Is_Binary_Operator (Expr) then
735 0
         DPE (PC_Check_Expression, EMC_Cannot_Parse_Check_Expression);
736 0
         Set_Last (First - 1);
737 0
         return No_Node;
738
      end if;
739

740
      Set_Left_Expr (Expr, Table (Last));
741
      Table (Last) := Expr;
742

743
      --  Push expressions in stack and check that the top of the
744
      --  stack consists in one or more binary operators with no
745
      --  right expr and zero or one expression value.
746

747 1
      while not Is_Expression_Completed loop
748

749 1
         Expr := P_Expression_Part;
750 1
         if No (Expr) then
751 0
            return No_Node;
752
         end if;
753

754 1
         Increment_Last;
755
         Table (Last) := Expr;
756

757
         --  Check that this new expression is not a binary operator
758
         --  when the previous one is a binary operator with no right
759
         --  expression.
760

761 1
         if First < Last
762 1
           and then Is_Binary_Operator (Expr)
763 1
           and then No (Left_Expr (Expr))
764
           and then Is_Binary_Operator (Table (Last - 1))
765
         then
766 0
            DPE (PC_Check_Expression, EMC_Cannot_Parse_Check_Expression);
767 0
            Set_Last (First - 1);
768 0
            return No_Node;
769
         end if;
770

771
         --  Check whether we have a sequence of a binary operator
772
         --  (left operator), an expression value and another binary
773
         --  operator (right operator). In this case, if the left
774
         --  operator has a better precedence than the right one, we
775
         --  can reduce the global expression by assigning the
776
         --  expression value to the right expression of the left
777
         --  operator. Then as the left operator has already a left
778
         --  expression, it becomes an expression value which can be
779
         --  assigned to the left expression of the right operation.
780
         --  Recompute the size of the expression stack.
781

782
         while First + 1 < Last
783
           and then Kind (Table (Last - 1)) /= K_Check_Subprogram_Call
784
           and then Is_Expression_Value (Table (Last - 1))
785
           and then Precede (Table (Last - 2), Expr)
786
         loop
787
            Set_Right_Expr (Table (Last - 2), Table (Last - 1));
788
            Set_Left_Expr (Table (Last), Table (Last - 2));
789
            Table (Last - 2) := Table (Last);
790
            Set_Last (Last - 2);
791 1
         end loop;
792 1
      end loop;
793

794
      --  The last expression is not a value. We cannot reduce the
795
      --  global expression
796

797
      if Is_Binary_Operator (Table (Last)) then
798 0
         DPE (PC_Check_Expression, EMC_Cannot_Parse_Check_Expression);
799 0
         Set_Last (First - 1);
800 0
         return No_Node;
801
      end if;
802

803
      --  Reduce the global expression
804

805 1
      while First < Last loop
806
         if No (Left_Expr (Table (Last - 1))) then
807
            Set_Right_Expr (Table (Last - 1), Table (Last));
808
            Set_Left_Expr (Table (Last - 1), Table (Last - 2));
809
            Table (Last - 2) := Table (Last - 1);
810
            Set_Last (Last - 2);
811

812
         else
813
            Set_Right_Expr (Table (Last - 1), Table (Last));
814
            Set_Last (Last - 1);
815
         end if;
816 1
      end loop;
817
      Expr := Table (First);
818
      Set_Last (First - 1);
819

820 1
      return Expr;
821
   end P_Check_Expression;
822

823
   --------------------------
824
   -- P_Ternary_Expression --
825
   --------------------------
826

827 1
   function P_Ternary_Expression return Node_Id is
828

829
      function Translate_Operator (T : Token_Type) return Operator_Id;
830

831
      ------------------------
832
      -- Translate_Operator --
833
      ------------------------
834

835 1
      function Translate_Operator (T : Token_Type) return Operator_Id is
836
      begin
837
         case T is
838
            when T_If =>
839 1
               return OV_If_Then_Else;
840
            when others =>
841 0
               return OV_Invalid;
842
         end case;
843
      end Translate_Operator;
844

845 1
      N  : Node_Id;
846 1
      E1 : Node_Id;
847 1
      E2 : Node_Id;
848 1
      E3 : Node_Id;
849
   begin
850 1
      N := New_Node (K_Ternary_Expression, Token_Location);
851

852 1
      Scan_Token;
853 1
      Set_Operator (N, Translate_Operator (Token));
854

855
      case Token is
856
         when T_If =>
857 1
            E1 := P_Expression;
858 1
            if No (E1) then
859 0
               return No_Node;
860
            end if;
861

862 1
            Scan_Token (T_Then);
863 1
            if Token = T_Error then
864 0
               DPE (PC_Ternary_Expression, T_Then);
865
            end if;
866

867 1
            E2 := P_Expression;
868 1
            if No (E2) then
869 0
               return No_Node;
870
            end if;
871

872 1
            Scan_Token (T_Else);
873 1
            if Token = T_Error then
874 0
               DPE (PC_Ternary_Expression, T_Else);
875
            end if;
876

877 1
            E3 := P_Expression;
878 1
            if No (E3) then
879 0
               return No_Node;
880
            end if;
881

882
         when others =>
883 0
            return No_Node;
884
      end case;
885

886 1
      Set_Left_Expr (N, E1);
887 1
      Set_Right_Expr (N, E2);
888 1
      Set_Third_Expr (N, E3);
889

890 1
      return N;
891
   end P_Ternary_Expression;
892

893
   ------------------
894
   -- P_Expression --
895
   ------------------
896

897 1
   function P_Expression return Node_Id is
898 1
      L : Location;
899
   begin
900 1
      Save_Lexer (L);
901 1
      Scan_Token;
902 1
      if Token = T_If then
903 1
         Restore_Lexer (L);
904 1
         return P_Ternary_Expression;
905
      else
906 1
         Restore_Lexer (L);
907 1
         return P_Check_Expression;
908
      end if;
909 1
   end P_Expression;
910

911
   -----------------------------
912
   -- P_Check_Subprogram_Call --
913
   -----------------------------
914

915 1
   function P_Check_Subprogram_Call return Node_Id is
916 1
      N     : Node_Id;
917 1
      L     : constant List_Id := New_List (K_List_Id, Token_Location);
918 1
      Param : Node_Id;
919
   begin
920 1
      N := New_Node (K_Check_Subprogram_Call, Token_Location);
921

922 1
      if Next_Token not in Verification_Function_Type
923
        and then Next_Token not in Selection_Function_Type
924
      then
925 0
         Scan_Token;
926 0
         DPE (PC_Check_Subprogram_Call, EMC_Expected_Predefined_Function_Name);
927 0
         return No_Node;
928
      end if;
929 1
      Set_Variable_Position (N, Value_Id (0));
930 1
      Set_Identifier (N, P_Identifier);
931 1
      Set_Code (N, Translate_Function_Code (Token));
932

933
      --  it's possible that a subprogram was called without args
934
      --  (eg. when passed as parameter)
935

936 1
      if Next_Token /= T_Left_Paren then
937 0
         Set_Parameters (N, No_List);
938 0
         return N;
939
      else
940
         --  No error possible
941

942 1
         Scan_Token (T_Left_Paren);
943
      end if;
944

945
      --  We parse all parameters
946

947 1
      while Next_Token /= T_Right_Paren loop
948

949 1
         if Next_Token = T_EOF then
950 0
            DPE (PC_Check_Subprogram_Call, T_Right_Paren);
951 0
            return No_Node;
952
         end if;
953

954
         --  We could have either a literal, a set name (identifier
955
         --  or predefined set) or a check expression.
956

957
         case Next_Token is
958

959 1
            when T_Get_Property_Value .. T_Sum =>
960

961
               --  Verification function name
962

963 1
               Param := P_Check_Subprogram_Call;
964 1
               Append_Node_To_List (Param, L);
965

966 0
            when T_Is_Subcomponent_Of .. T_Is_Connecting_To =>
967

968
               --  selection function name
969

970 0
               Param := P_Check_Subprogram_Call;
971 0
               Append_Node_To_List (Param, L);
972

973 1
            when T_Processor_Set .. T_Local_Set =>
974

975
               --  We build a set reference with predefined name
976

977 1
               Scan_Token;
978 1
               Param := New_Node (K_Set_Reference, Token_Location);
979 1
               Set_Name (Param, To_Lower (Token_Name));
980 1
               Set_Predefined_Type (Param, Translate_Predefined_Sets (Token));
981 1
               Set_Referenced_Set (Param, No_Node);
982 1
               Append_Node_To_List (Param, L);
983

984 1
            when T_Identifier =>
985

986
               --  Must be a set name or the global set identifier or
987
               --  a variable name
988

989 1
               Scan_Token;
990 1
               Param := New_Node (K_Identifier, Token_Location);
991 1
               Set_Name (Param, Token_Name);
992 1
               Append_Node_To_List (Param, L);
993

994 1
            when T_Integer_Literal .. T_Wide_String_Literal =>
995

996
               --  A literal
997

998 1
               Scan_Token;
999 1
               Param := Make_Literal (Token);
1000 1
               Append_Node_To_List (Param, L);
1001

1002 1
            when T_Left_Paren =>
1003

1004
               --  A selection expression
1005

1006 1
               Param := Create_Check_Expression;
1007 1
               Append_Node_To_List (Param, L);
1008

1009 0
            when others =>
1010 0
               DPE
1011
                 (PC_Check_Subprogram_Call,
1012
                  EMC_Expected_Valid_Function_Parameter);
1013 0
               return No_Node;
1014
         end case;
1015

1016 1
         if Next_Token /= T_Comma then
1017

1018 1
            if Next_Token /= T_Right_Paren then
1019 0
               Scan_Token;
1020 0
               DPE (PC_Check_Subprogram_Call, T_Right_Paren);
1021 0
               return No_Node;
1022
            end if;
1023
         else
1024
            --  We pass the comma, no error possible
1025

1026 1
            Scan_Token (T_Comma);
1027
         end if;
1028

1029 1
      end loop;
1030

1031 1
      Scan_Token (T_Right_Paren);
1032 1
      if Token = T_Error then
1033 0
         DPE (PC_Check_Subprogram_Call, T_Right_Paren);
1034 0
         return No_Node;
1035
      end if;
1036

1037 1
      Set_Parameters (N, L);
1038 1
      return N;
1039

1040
   end P_Check_Subprogram_Call;
1041

1042
   ------------------
1043
   -- Make_Literal --
1044
   ------------------
1045

1046 1
   function Make_Literal (T : Token_Type) return Node_Id is
1047
      use Ocarina.REAL_Values;
1048

1049 1
      Const : constant Node_Id := New_Node (K_Literal, Token_Location);
1050
   begin
1051
      case T is
1052 1
         when T_String_Literal | T_Wide_String_Literal =>
1053 1
            Set_Value
1054
              (Const,
1055 1
               New_String_Value (To_Lower (String_Literal_Value)));
1056

1057 0
         when T_True =>
1058 0
            Set_Value (Const, New_Boolean_Value (True));
1059

1060 0
         when T_False =>
1061 0
            Set_Value (Const, New_Boolean_Value (False));
1062

1063 1
         when T_Integer_Literal =>
1064 1
            Set_Value
1065
              (Const,
1066
               New_Integer_Value
1067
                 (Value => Unsigned_Long_Long (Integer_Literal_Value),
1068
                  Base  => Unsigned_Short_Short (Integer_Literal_Base)));
1069

1070 1
         when T_Floating_Point_Literal =>
1071 1
            Set_Value (Const, New_Real_Value (Float_Literal_Value));
1072

1073 0
         when others =>
1074 0
            DPE (PC_Make_Literal, EMC_Expected_Literal_Value);
1075 0
            return No_Node;
1076
      end case;
1077

1078 1
      return Const;
1079
   end Make_Literal;
1080

1081
   -----------------------------
1082
   -- P_Create_Set_Identifier --
1083
   -----------------------------
1084

1085 1
   function P_Create_Set_Identifier return Node_Id is
1086 1
      N     : Node_Id;
1087 1
      Ident : Node_Id;
1088 1
      Param : Node_Id := No_Node;
1089 1
      L     : List_Id := No_List;
1090
   begin
1091
      --  Set identifier can be either parametrized
1092
      --  or not
1093

1094
      --  First we read the set identifier
1095

1096 1
      Ident := P_Identifier;
1097 1
      if No (Ident) then
1098 0
         return No_Node;
1099
      end if;
1100

1101
      --  Then if we have a left parenthesis
1102
      --  the set is parametrized by an identifier
1103

1104 1
      if Next_Token = T_Left_Paren then
1105

1106
         --  We skip the '('
1107 1
         Scan_Token;
1108

1109 1
         Param := P_Identifier;
1110

1111 1
         if No (Param) then
1112 0
            return No_Node;
1113
         end if;
1114

1115 1
         Scan_Token (T_Right_Paren);
1116 1
         if Token = T_Error then
1117 0
            DPE (PC_Create_Set_Identifier, T_Right_Paren);
1118 0
            return No_Node;
1119
         end if;
1120

1121 1
         L := New_List (K_List_Id, Token_Location);
1122 1
         Append_Node_To_List (Param, L);
1123
      end if;
1124

1125 1
      N := New_Node (K_Parametrized_Identifier, Token_Location);
1126 1
      Set_Identifier (N, Ident);
1127 1
      Set_Parameters (N, L);
1128

1129 1
      return N;
1130
   end P_Create_Set_Identifier;
1131

1132
   ------------------------------
1133
   -- P_Single_Var_Declaration --
1134
   ------------------------------
1135

1136 1
   function P_Single_Var_Declaration return Node_Id is
1137 1
      Var_Decl : Node_Id;
1138 1
      Var_Id   : Node_Id;
1139 1
      Var, P   : Node_Id;
1140 1
      Trm_Id   : Node_Id;
1141 1
      Params   : List_Id := No_List;
1142 1
      Global   : Boolean;
1143
   begin
1144
      --  Parse the variable range keyword (var or global)
1145

1146 1
      Scan_Token;
1147
      case Token is
1148 1
         when T_Var =>
1149 1
            Global := False;
1150 1
         when T_Global =>
1151 1
            Global := True;
1152 0
         when others =>
1153 0
            DPE (PC_Single_Variable_Declaration, EMC_Variable_Declaration);
1154 0
            return No_Node;
1155 1
      end case;
1156

1157
      --  Create variable identifier
1158

1159 1
      Var_Id := P_Identifier;
1160 1
      if No (Var_Id) then
1161 0
         return No_Node;
1162
      end if;
1163 1
      Var := Make_Var_Reference (Name (Var_Id));
1164

1165
      --  Parse the affectation (":=")
1166

1167 1
      Scan_Token (T_Affect);
1168 1
      if Token = T_Error then
1169 0
         DPE (PC_Single_Variable_Declaration, T_Affect);
1170 0
         return No_Node;
1171
      end if;
1172

1173
      --  A variable declaration can be done either with
1174
      --  a expression or with a call to another theorem
1175

1176 1
      if Next_Token = T_Compute then
1177 1
         Scan_Token (T_Compute);
1178

1179 1
         Var_Decl := New_Node (K_Variable_Decl_Compute, Token_Location);
1180

1181 1
         Trm_Id := P_Identifier;
1182 1
         if No (Trm_Id) then
1183 0
            return No_Node;
1184
         end if;
1185

1186 1
         if Next_Token = T_Left_Paren then
1187 1
            Scan_Token (T_Left_Paren);
1188 1
            Params := New_List (K_List_Id, Token_Location);
1189

1190
            --  The first parameter must be the sub-theorem domain
1191
            --  Thus a set or a variable
1192

1193
            case Next_Token is
1194

1195 1
               when T_Identifier =>
1196 1
                  Scan_Token;
1197 1
                  P := New_Node (K_Identifier, Token_Location);
1198 1
                  Set_Name (P, To_Lower (Token_Name));
1199 1
                  Append_Node_To_List (P, Params);
1200

1201 0
               when T_Processor_Set .. T_Local_Set =>
1202 0
                  Scan_Token;
1203 0
                  P := New_Node (K_Set_Reference, Token_Location);
1204 0
                  Set_Name (P, To_Lower (Token_Name));
1205 0
                  Set_Predefined_Type (P, Translate_Predefined_Sets (Token));
1206 0
                  Set_Referenced_Set (P, No_Node);
1207 0
                  Append_Node_To_List (P, Params);
1208

1209 0
               when others =>
1210 0
                  DPE
1211
                    (PC_Single_Variable_Declaration,
1212
                     EMC_Subtheorem_Parameter);
1213 0
                  return No_Node;
1214
            end case;
1215

1216 1
            if Next_Token = T_Comma then
1217 1
               Scan_Token (T_Comma);
1218

1219
               --  We parse all others parameters
1220

1221 1
               while Next_Token /= T_Right_Paren loop
1222

1223
                  --  We could have either a literal, or a variable
1224

1225
                  case Next_Token is
1226

1227 0
                     when T_EOF =>
1228 0
                        DPE
1229
                          (PC_Single_Variable_Declaration,
1230
                           EMC_Unexpected_Error);
1231 0
                        return No_Node;
1232

1233 1
                     when T_Integer_Literal .. T_Wide_String_Literal =>
1234 1
                        Scan_Token;
1235 1
                        P := Make_Literal (Token);
1236 1
                        Append_Node_To_List (P, Params);
1237

1238 1
                     when T_Identifier =>
1239 1
                        Scan_Token;
1240 1
                        P := New_Node (K_Identifier, Token_Location);
1241 1
                        Set_Name (P, To_Lower (Token_Name));
1242 1
                        Append_Node_To_List (P, Params);
1243

1244 0
                     when others =>
1245 0
                        DPE
1246
                          (PC_Single_Variable_Declaration,
1247
                           EMC_Unexpected_Token);
1248 0
                        return No_Node;
1249 1
                  end case;
1250

1251 1
                  if Next_Token /= T_Comma then
1252

1253 1
                     if Next_Token /= T_Right_Paren then
1254 0
                        Scan_Token;
1255 0
                        DPE (PC_Single_Variable_Declaration, T_Comma);
1256 0
                        return No_Node;
1257
                     end if;
1258
                  else
1259
                     --  We pass the comma, no error possible
1260 1
                     Scan_Token (T_Comma);
1261
                  end if;
1262 1
               end loop;
1263
            end if;
1264

1265 1
            Scan_Token (T_Right_Paren);
1266 1
            if Token = T_Error then
1267 0
               DPE (PC_Single_Variable_Declaration, T_Right_Paren);
1268 0
               return No_Node;
1269
            end if;
1270
         end if;
1271

1272 1
         Set_Parameters (Var_Decl, Params);
1273 1
         Set_True_params (Var_Decl, No_List);
1274 1
         Set_Domain (Var_Decl, No_Node);
1275 1
         Set_Var_Ref (Var_Decl, Var);
1276 1
         Set_Theorem_Name (Var_Decl, Name (Trm_Id));
1277
      else
1278
         declare
1279
            use Ocarina.REAL_Values;
1280 1
            D, C : Node_Id;
1281 1
            V    : Value_Id := No_Value;
1282 1
            L    : Location;
1283
         begin
1284 1
            Var_Decl := New_Node (K_Variable_Decl_Expression, Token_Location);
1285

1286 1
            D := New_Node (K_Return_Expression, Token_Location);
1287

1288 1
            Save_Lexer (L);
1289 1
            Scan_Token;
1290 1
            if Token in Higher_Level_Function_Type then
1291 0
               V := Translate_Function_Code (Token);
1292 0
               Set_Range_Function (D, V);
1293
            else
1294 1
               Restore_Lexer (L);
1295
            end if;
1296

1297 1
            C := P_Expression;
1298

1299 1
            Set_Check_Expression (D, C);
1300 1
            Set_Return_Expr (Var_Decl, D);
1301 1
            Set_Var_Ref (Var_Decl, Var);
1302 1
         end;
1303
      end if;
1304

1305 1
      Scan_Token (T_Semi_Colon);
1306 1
      if Token = T_Error then
1307 0
         DPE (PC_Single_Variable_Declaration, T_Semi_Colon);
1308 0
         return No_Node;
1309
      end if;
1310

1311
      --  Set scope status
1312

1313 1
      if Global then
1314 1
         Set_Is_Global (Var_Decl, Value_Id (1));
1315
      else
1316 1
         Set_Is_Global (Var_Decl, Value_Id (0));
1317
      end if;
1318

1319 1
      return Var_Decl;
1320
   end P_Single_Var_Declaration;
1321

1322
   ------------------------------
1323
   -- P_Single_Set_Declaration --
1324
   ------------------------------
1325

1326 1
   function P_Single_Set_Declaration return Node_Id is
1327 1
      Set_Decl     : Node_Id;
1328 1
      Set_Id       : Node_Id;
1329 1
      Set_Expr     : Node_Id;
1330 1
      Set_Def      : Node_Id;
1331 1
      State        : Location;
1332 1
      State_2      : Location;
1333 1
      Is_Dependant : Boolean := False;
1334
   begin
1335

1336
      --  We parse the set name
1337
      --  wich can be parametrized
1338

1339 1
      Save_Lexer (State);
1340 1
      Set_Id := P_Create_Set_Identifier;
1341 1
      if No (Set_Id) then
1342 0
         return No_Node;
1343
      end if;
1344

1345
      --  We check weither the declared set is parametrized or not
1346

1347 1
      Save_Lexer (State_2);
1348 1
      Restore_Lexer (State);
1349 1
      Scan_Token (T_Identifier);
1350 1
      Scan_Token;
1351 1
      if Token = T_Left_Paren then
1352 1
         Is_Dependant := True;
1353
      end if;
1354 1
      Restore_Lexer (State_2);
1355

1356
      --  Then we should have ':=' token
1357

1358 1
      Scan_Token (T_Affect);
1359 1
      if Token = T_Error then
1360 0
         DPE (PC_Single_Set_Declaration, T_Affect);
1361 0
         return No_Node;
1362
      end if;
1363

1364
      --  We enter braces
1365

1366 1
      Scan_Token (T_Left_Brace);
1367 1
      if Token = T_Error then
1368 0
         DPE (PC_Single_Set_Declaration, T_Left_Brace);
1369 0
         return No_Node;
1370
      end if;
1371

1372 1
      Set_Decl := New_Node (K_Set_Declaration, Token_Location);
1373 1
      Set_Parametrized_Expr (Set_Decl, Set_Id);
1374 1
      if Is_Dependant then
1375 1
         Set_Dependant (Set_Decl, Value_Id (1));
1376
      else
1377 1
         Set_Dependant (Set_Decl, Value_Id (0));
1378
      end if;
1379

1380
      --  Parse the local variable
1381

1382 1
      Set_Local_Variable (Set_Decl, Make_Var_Reference (Name (P_Identifier)));
1383 1
      if Token = T_Error then
1384 0
         DPE (PC_Single_Set_Declaration, EMC_Unexpected_Error);
1385 0
         return No_Node;
1386
      end if;
1387

1388
      --  Then we should have 'in' token
1389

1390 1
      Scan_Token (T_In);
1391 1
      if Token = T_Error then
1392 0
         DPE (PC_Single_Set_Declaration, T_In);
1393 0
         return No_Node;
1394
      end if;
1395

1396
      --  We parse the set expression
1397

1398 1
      Set_Expr := P_Set_Expression;
1399 1
      Set_Local_Set_Expression (Set_Decl, Set_Expr);
1400

1401
      --  We pass the sothat
1402

1403 1
      Scan_Token (T_Sothat);
1404

1405 1
      if Token = T_Error then
1406 0
         DPE (PC_Single_Set_Declaration, T_Sothat);
1407 0
         return No_Node;
1408
      end if;
1409

1410
      --  We parse set definition
1411

1412 1
      Set_Def := P_Expression;
1413 1
      if No (Set_Def) then
1414 0
         return No_Node;
1415
      end if;
1416

1417 1
      Set_Selection_Expression (Set_Decl, Set_Def);
1418

1419
      --  We read the right brace (exit of set declaration)
1420

1421 1
      Scan_Token (T_Right_Brace);
1422 1
      if Token = T_Error then
1423 0
         DPE (PC_Single_Set_Declaration, T_Right_Brace);
1424 0
         return No_Node;
1425
      end if;
1426

1427
      --  We pass the semi-colon
1428

1429 1
      Scan_Token (T_Semi_Colon);
1430 1
      if Token = T_Error then
1431 0
         DPE (PC_Single_Set_Declaration, T_Semi_Colon);
1432 0
         return No_Node;
1433
      end if;
1434

1435 1
      return Set_Decl;
1436 1
   end P_Single_Set_Declaration;
1437

1438
   --------------------
1439
   -- P_Requirements --
1440
   --------------------
1441

1442 1
   function P_Requirements return List_Id is
1443 1
      L : constant List_Id := New_List (K_List_Id, Token_Location);
1444 1
      P : Node_Id;
1445
   begin
1446

1447 1
      if Next_Token /= T_Requires then
1448 1
         return L;
1449
      else
1450 1
         Scan_Token;
1451
      end if;
1452

1453 1
      Scan_Token (T_Left_Paren);
1454 1
      if Token = T_Error then
1455 0
         DPE (PC_Requirements_List, T_Left_Paren);
1456 0
         return No_List;
1457
      end if;
1458

1459
      loop
1460 1
         Scan_Token (T_Identifier);
1461 1
         if Token = T_Error then
1462 0
            DPE (PC_Requirements_List, T_Identifier);
1463 0
            return No_List;
1464
         end if;
1465

1466 1
         P := New_Node (K_Required_Theorem, Token_Location);
1467 1
         Set_Theorem_Name (P, To_Lower (Token_Name));
1468 1
         Append_Node_To_List (P, L);
1469

1470 1
         Scan_Token;
1471

1472
         case Token is
1473 1
            when T_And =>
1474 1
               null;
1475

1476 1
            when T_Right_Paren =>
1477 1
               exit;
1478

1479 0
            when others =>
1480 0
               DPE (PC_Requirements_List, EMC_Wrong_List_Connector);
1481 0
               return No_List;
1482 1
         end case;
1483

1484 1
      end loop;
1485

1486 1
      Scan_Token (T_Semi_Colon);
1487 1
      if Token = T_Error then
1488 0
         DPE (PC_Requirements_List, T_Semi_Colon);
1489 0
         return No_List;
1490
      end if;
1491

1492 1
      return L;
1493
   end P_Requirements;
1494

1495
   --------------------
1496
   -- P_Declarations --
1497
   --------------------
1498

1499 1
   procedure P_Declarations (R : Node_Id; Success : out Boolean) is
1500
      pragma Assert (Kind (R) = K_Theorem);
1501

1502
      Declarations_List : constant List_Id :=
1503 1
        New_List (K_List_Id, Token_Location);
1504 1
      Declaration : Node_Id := No_Node;
1505 1
      Stop        : Boolean := False;
1506
   begin
1507 1
      Success := True;
1508 1
      while not Stop and then Success loop
1509

1510
         case Next_Token is
1511

1512 1
            when T_Identifier =>  --  Set declaration
1513 1
               Declaration := P_Single_Set_Declaration;
1514 1
               if No (Declaration) then
1515 0
                  Success := False;
1516
               else
1517 1
                  Append_Node_To_List (Declaration, Declarations_List);
1518
               end if;
1519

1520 1
            when T_Var | T_Global =>  --  Variable declaration
1521 1
               Declaration := P_Single_Var_Declaration;
1522 1
               if No (Declaration) then
1523 0
                  Success := False;
1524
               else
1525 1
                  Append_Node_To_List (Declaration, Declarations_List);
1526
               end if;
1527

1528 1
            when T_Return | T_Requires | T_Check =>
1529 1
               Stop := True;
1530

1531 0
            when others =>
1532 0
               DPE (PC_Declarations_List, EMC_Declaration_Parameter);
1533 0
               Success := False;
1534
         end case;
1535

1536 1
      end loop;
1537

1538 1
      if Success then
1539 1
         Set_Declarations (R, Declarations_List);
1540
      end if;
1541 1
   end P_Declarations;
1542

1543
   -----------------------------
1544
   -- Create_Check_Expression --
1545
   -----------------------------
1546

1547 1
   function Create_Check_Expression return Node_Id is
1548 1
      N : Node_Id;
1549
   begin
1550
      --  We pass the left parenthesis
1551

1552 1
      Scan_Token (T_Left_Paren);
1553 1
      if Token = T_Error then
1554 0
         DPE (PC_Create_Check_Expression, T_Left_Paren);
1555 0
         return No_Node;
1556
      end if;
1557

1558 1
      N := P_Expression;
1559 1
      if No (N) then
1560 0
         return No_Node;
1561
      end if;
1562

1563
      --  We pass the right parenthesis
1564

1565 1
      Scan_Token (T_Right_Paren);
1566 1
      if Token = T_Error then
1567 0
         DPE (PC_Create_Check_Expression, T_Right_Paren);
1568 0
         return No_Node;
1569
      end if;
1570

1571 1
      return N;
1572
   end Create_Check_Expression;
1573

1574
   ------------------
1575
   -- P_Identifier --
1576
   ------------------
1577

1578 1
   function P_Identifier return Node_Id is
1579 1
      Identifier : Node_Id;
1580

1581
   begin
1582 1
      Scan_Token;
1583

1584 1
      if Token /= T_Identifier
1585 1
        and then Token not in Selection_Function_Type
1586 1
        and then Token not in Verification_Function_Type
1587
      then
1588 0
         DPE (PC_Identifier_Declaration, EMC_Used_Keyword);
1589 0
         return No_Node;
1590
      end if;
1591 1
      Identifier := New_Node (K_Identifier, Token_Location);
1592 1
      Set_Name (Identifier, To_Lower (Token_Name));
1593 1
      return Identifier;
1594
   end P_Identifier;
1595

1596
   -----------------------------
1597
   -- P_Set_Range_Declaration --
1598
   -----------------------------
1599

1600 1
   function P_Set_Range_Declaration return Node_Id is
1601 1
      Range_Decl : Node_Id;
1602 1
      Identifier : Node_Id;
1603 1
      Elem       : Node_Id;
1604 1
      Set_Expr   : Node_Id;
1605
   begin
1606 1
      Range_Decl := New_Node (K_Range_Declaration, Token_Location);
1607

1608
      --  Scan 'foreach'
1609

1610 1
      Scan_Token (T_Foreach);
1611 1
      if Token = T_Error then
1612 0
         DPE (PC_Set_Declarations, T_Foreach);
1613 0
         return No_Node;
1614
      end if;
1615

1616
      --  Scan the element name
1617

1618 1
      Identifier := P_Identifier;
1619 1
      if No (Identifier) then
1620 0
         DPE (PC_Set_Declarations, T_Identifier);
1621 0
         return No_Node;
1622
      end if;
1623

1624 1
      Elem := New_Node (K_Element, Token_Location);
1625 1
      Set_Identifier (Elem, Identifier);
1626 1
      Set_Element_Type (Elem, SV_No_Type);
1627

1628
      --  Scan 'in'
1629

1630 1
      Scan_Token (T_In);
1631 1
      if Token = T_Error then
1632 0
         DPE (PC_Set_Declarations, T_In);
1633 0
         return No_Node;
1634
      end if;
1635

1636 1
      Set_Expr := P_Set_Expression;
1637 1
      if No (Set_Expr) then
1638 0
         return No_Node;
1639
      end if;
1640

1641
      --  Scan 'do'
1642

1643 1
      Scan_Token (T_Do);
1644 1
      if Token = T_Error then
1645 0
         DPE (PC_Set_Declarations, T_Do);
1646 0
         return No_Node;
1647
      end if;
1648

1649 1
      Set_Range_Variable (Range_Decl, Elem);
1650 1
      Set_Range_Set (Range_Decl, Set_Expr);
1651 1
      Set_Variable_Ref
1652
        (Range_Decl,
1653 1
         New_Node (K_Var_Reference, Token_Location));
1654

1655 1
      return Range_Decl;
1656
   end P_Set_Range_Declaration;
1657

1658
   -----------------------------
1659
   -- P_Higher_Level_Function --
1660
   -----------------------------
1661

1662 1
   function P_Higher_Level_Function return Value_Id is
1663
      use Ocarina.REAL_Values;
1664

1665 1
      State : Location;
1666 1
      V     : Value_Id := No_Value;
1667
   begin
1668 1
      Save_Lexer (State);
1669

1670 1
      Scan_Token (T_Left_Paren);
1671 1
      if Token = T_Error then
1672 0
         DPE (PC_Function, T_Left_Paren);
1673 0
         Restore_Lexer (State);
1674 0
         return No_Value;
1675
      end if;
1676

1677 1
      Scan_Token;
1678 1
      if Token in Higher_Level_Function_Type then
1679 1
         V := Translate_Function_Code (Token);
1680
      else
1681 1
         Restore_Lexer (State);
1682
      end if;
1683

1684 1
      return V;
1685 1
   end P_Higher_Level_Function;
1686

1687
   ---------------
1688
   -- P_Theorem --
1689
   ---------------
1690

1691 1
   function P_Theorem return Node_Id is
1692
      use Ocarina.REAL_Values;
1693

1694 1
      Node         : Node_Id;
1695 1
      Identifier   : Node_Id;
1696 1
      Range_Decl   : Node_Id;
1697 1
      Test         : Node_Id;
1698 1
      Returns      : Node_Id;
1699 1
      Requirements : List_Id;
1700 1
      V            : Value_Id;
1701 1
      Success      : Boolean;
1702
   begin
1703 1
      Node := New_Node (K_Theorem, Token_Location);
1704 1
      Set_Used_Set (Node, New_List (K_List_Id, Token_Location));
1705 1
      Set_Used_Var (Node, New_List (K_List_Id, Token_Location));
1706 1
      Set_Local_Var (Node, New_List (K_List_Id, Token_Location));
1707

1708 1
      Scan_Token;
1709 1
      Identifier := New_Node (K_Identifier, Token_Location);
1710 1
      Set_Name (Identifier, To_Lower (Token_Name));
1711 1
      Set_Identifier (Node, Identifier);
1712 1
      Set_Related_Entity (Node, Owner_Node);
1713 1
      Current_Theorem_Name := Name (Identifier);
1714

1715
      --  This line allow to find back the theorem's name
1716

1717 1
      Current_Theorem_Node := Node;
1718

1719 1
      Range_Decl := P_Set_Range_Declaration;
1720

1721 1
      if No (Range_Decl) then
1722 0
         return No_Node;
1723
      else
1724 1
         Set_Range_Declaration (Node, Range_Decl);
1725
      end if;
1726

1727 1
      P_Declarations (Node, Success);
1728

1729 1
      if not Success then
1730 0
         return No_Node;
1731
      end if;
1732

1733 1
      Requirements := P_Requirements;
1734 1
      if Requirements /= No_List then
1735 1
         Set_Required_Theorems (Node, Requirements);
1736
      else
1737 0
         return No_Node;
1738
      end if;
1739

1740
      --  Here we have either a check or a return token
1741 1
      Scan_Token;
1742 1
      if Token /= T_Check and then Token /= T_Return then
1743 0
         DPE (PC_Theorem, EMC_Testing_Token_Expected);
1744 0
         return No_Node;
1745
      end if;
1746

1747 1
      if Token = T_Check then
1748 1
         Test := Create_Check_Expression;
1749 1
         if No (Test) then
1750 0
            return No_Node;
1751
         else
1752 1
            Set_Check_Expression (Node, Test);
1753
         end if;
1754

1755 1
         Set_Return_Expression (Node, No_Node);
1756
      else
1757
         --  Return expression
1758
         --  "return expressions" are actually the same
1759
         --  as "check expressions"
1760

1761 1
         Returns := New_Node (K_Return_Expression, Token_Location);
1762 1
         V       := P_Higher_Level_Function;
1763 1
         Set_Range_Function (Returns, V);
1764

1765 1
         Test := Create_Check_Expression;
1766

1767 1
         if V /= No_Value then
1768 1
            Scan_Token (T_Right_Paren);
1769 1
            if Token = T_Error then
1770 0
               DPE (PC_Theorem, T_Right_Paren);
1771 0
               return No_Node;
1772
            end if;
1773
         end if;
1774

1775 1
         if No (Test) then
1776 0
            return No_Node;
1777
         else
1778 1
            Set_Check_Expression (Returns, Test);
1779 1
            Set_Return_Expression (Node, Returns);
1780
         end if;
1781 1
         Set_Check_Expression (Node, No_Node);
1782
      end if;
1783

1784
      --  We pass the semi-colon
1785

1786 1
      Scan_Token;
1787 1
      if Token /= T_Semi_Colon then
1788 0
         DPE (PC_Theorem, T_Semi_Colon);
1789 0
         return No_Node;
1790
      end if;
1791

1792 1
      return Node;
1793
   end P_Theorem;
1794

1795
   -------------------------
1796
   -- Skip_To_Theorem_End --
1797
   -------------------------
1798

1799 1
   procedure Skip_To_Theorem_End (Success : out Boolean) is
1800 1
      End_Found : Boolean := (Token = T_End);
1801
   begin
1802 1
      Success := True;
1803

1804
      --  FIXME :
1805
      --  put back all references to scan_token (x) => scan_token in parser,
1806
      --  in Order To Be Able To Find Back The "end" Keyword when It Was
1807
      --  Unexpectedly Parsed.
1808

1809 1
      while not End_Found loop
1810 1
         Scan_Token;
1811

1812 1
         exit when Token = T_EOF;
1813

1814 1
         if Token = T_End then
1815 1
            End_Found := True;
1816
         end if;
1817 1
      end loop;
1818

1819 1
      if not End_Found then
1820 0
         DPE (PC_Main, T_End);
1821 0
         Success := False;
1822 0
         return;
1823
      end if;
1824

1825 1
      Scan_Token;
1826
      case Token is
1827

1828 1
         when T_Identifier =>
1829 1
            if To_Lower (Token_Name) /= Current_Theorem_Name then
1830 0
               DPE (PC_Main, EMC_Non_Matching_Theorem_Name);
1831 0
               Success := False;
1832 0
               return;
1833
            end if;
1834 1
            Scan_Token (T_Semi_Colon);
1835 1
            if Token = T_Error then
1836 0
               DPE (PC_Main, T_Semi_Colon);
1837 0
               Success := False;
1838 0
               return;
1839
            end if;
1840

1841 1
         when T_Semi_Colon =>
1842 1
            return;
1843

1844 0
         when others =>
1845 0
            DPE (PC_Main, T_Semi_Colon);
1846 0
            Success := False;
1847 0
            return;
1848 1
      end case;
1849

1850 1
   end Skip_To_Theorem_End;
1851

1852
   -------------
1853
   -- Process --
1854
   -------------
1855

1856 1
   function Process
1857
     (AADL_Root : Node_Id;
1858
      From      : Location;
1859
      To        : Location := No_Location;
1860
      Container : Node_Id  := No_Node) return Node_Id
1861
   is
1862
      pragma Unreferenced (AADL_Root);
1863
      pragma Unreferenced (Container);
1864

1865 1
      Buffer  : Location;
1866 1
      Root    : constant Node_Id := New_Node (K_Root_Node, From);
1867 1
      N       : Node_Id;
1868 1
      Success : Boolean          := True;
1869 1
      State   : Location;
1870
   begin
1871 1
      Buffer := From;
1872

1873
      if To /= No_Location then
1874 0
         Buffer.EOF := To.Last_Pos;
1875
      end if;
1876

1877 1
      Restore_Lexer (Buffer);
1878

1879 1
      Set_Theorems (Root, New_List (K_List_Id, From));
1880

1881 1
      Scan_Token;
1882

1883 1
      while Token = T_Theorem loop
1884 1
         N := P_Theorem;
1885

1886 1
         Skip_To_Theorem_End (Success);
1887

1888 1
         if No (N) or else not Success then
1889 0
            N := Current_Theorem_Node;
1890 0
            DPE (PC_Main, EMC_Syntax_Error);
1891 0
            Success := False;
1892 0
            exit;
1893
         end if;
1894

1895 1
         Append_Node_To_List (N, Theorems (Root));
1896

1897
         --  Pass to the next theorem
1898

1899 1
         Save_Lexer (State);
1900 1
         Scan_Token;
1901 1
      end loop;
1902

1903 1
      if Success then
1904 1
         if Token /= T_EOF then
1905 0
            DPE (PC_Main, T_EOF);
1906 0
            return No_Node;
1907
         end if;
1908

1909
         --  the AADL main parser need the EOF ("**}") token to be the
1910
         --  first lexem available after a successful annex parsing
1911

1912 1
         Restore_Lexer (State);
1913

1914 1
         return Root;
1915
      else
1916 0
         DPE (PC_Main, EMC_Syntax_Error);
1917 0
         return No_Node;
1918
      end if;
1919 1
   end Process;
1920

1921
   -----------------------
1922
   -- Load_REAL_Library --
1923
   -----------------------
1924

1925 1
   procedure Load_REAL_Library (File_Name : Name_Id) is
1926
      use Ocarina.Files;
1927
      use Ocarina.Namet;
1928

1929 1
      Buffer            : Location;
1930 1
      REAL_External_Lib : Node_Id;
1931
   begin
1932 1
      Buffer := Load_File (File_Name);
1933
      if Buffer = No_Location then
1934
         Display_And_Exit
1935
           ("could not load file " &
1936 1
              Get_Name_String (File_Name));
1937
      end if;
1938

1939 1
      REAL_External_Lib := Process (No_Node, Buffer);
1940 1
      if No (REAL_External_Lib) then
1941 0
         Display_And_Exit ("could not parse REAL specification");
1942
      end if;
1943

1944 1
      Register_Library_Theorems (REAL_External_Lib);
1945
   end Load_REAL_Library;
1946

1947
   ----------
1948
   -- Init --
1949
   ----------
1950

1951 1
   procedure Init is
1952
      use Ocarina.Parser;
1953
      use Ocarina.Namet;
1954

1955
   begin
1956 1
      Current_Theorem_Node := No_Node;
1957

1958 1
      REAL_Language := Get_String_Name (Language);
1959 1
      Register_Parser (Ocarina.ME_REAL.Tokens.Language, Process'Access);
1960

1961
      --  If a REAL library file had been defined, we
1962
      --  parse and register it.
1963

1964
      for J in REAL_Libs.First .. REAL_Libs.Last loop
1965
         Load_REAL_Library (REAL_Libs.Table (J));
1966 1
      end loop;
1967 1
   end Init;
1968

1969 1
end Ocarina.FE_REAL.Parser;

Read our documentation on viewing source code .

Loading