with PSL.Errors; use PSL.Errors;
with Types; use Types;

package body PSL.Subsets is
   procedure Check_Simple (N : Node)
   is
   begin
      case Get_Kind (N) is
         when N_Not_Bool =>
            if Get_Psl_Type (Get_Boolean (N)) /= Type_Boolean then
               Error_Msg_Sem
                 ("operand of a negation operator must be a boolean", N);
            end if;
         when N_Never =>
            case Get_Psl_Type (Get_Property (N)) is
               when Type_Sequence | Type_Boolean =>
                  null;
               when others =>
                  Error_Msg_Sem ("operand of a 'never' operator must be "
                                   & "a boolean or a sequence", N);
            end case;
         when N_Eventually =>
            case Get_Psl_Type (Get_Property (N)) is
               when Type_Sequence | Type_Boolean =>
                  null;
               when others =>
                  Error_Msg_Sem ("operand of an 'eventually!' operator must be"
                                   & " a boolean or a sequence", N);
            end case;
         when N_And_Bool =>
            if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then
               Error_Msg_Sem ("left-hand side operand of logical 'and' must be"
                                & " a boolean", N);
            end if;
         when N_Or_Bool =>
            if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then
               Error_Msg_Sem ("left-hand side operand of logical 'or' must be"
                                & " a boolean", N);
            end if;
         when N_Log_Imp_Prop =>
            if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then
               Error_Msg_Sem ("left-hand side operand of logical '->' must be"
                                & " a boolean", N);
            end if;
            --  FIXME: <->
         when N_Until =>
            if not Get_Inclusive_Flag (N) then
               if Get_Psl_Type (Get_Right (N)) /= Type_Boolean then
                  Error_Msg_Sem ("right-hand side of a non-overlapping "
                                   & "'until*' operator must be a boolean", N);
               end if;
            else
               if Get_Psl_Type (Get_Right (N)) /= Type_Boolean
                 or else Get_Psl_Type (Get_Left (N)) /= Type_Boolean
               then
                  Error_Msg_Sem ("both operands of an overlapping 'until*'"
                                   & " operator are boolean", N);
               end if;
            end if;
         when N_Before =>
            if Get_Psl_Type (Get_Right (N)) /= Type_Boolean
              or else Get_Psl_Type (Get_Left (N)) /= Type_Boolean
            then
               Error_Msg_Sem ("both operands of a 'before*'"
                                & " operator are boolean", N);
            end if;
         when others =>
            null;
      end case;

      --  Recursion.
      case Get_Kind (N) is
         when N_Error =>
            null;
         when N_Hdl_Mod_Name =>
            null;
         when N_Vunit
           | N_Vmode
           | N_Vprop =>
            declare
               Item : Node;
            begin
               Item := Get_Item_Chain (N);
               while Item /= Null_Node loop
                  Check_Simple (Item);
                  Item := Get_Chain (Item);
               end loop;
            end;
         when N_Name_Decl =>
            null;
         when N_Assert_Directive
           | N_Property_Declaration =>
            Check_Simple (Get_Property (N));
         when N_Endpoint_Declaration
           | N_Sequence_Declaration =>
            Check_Simple (Get_Sequence (N));
         when N_Clock_Event =>
            Check_Simple (Get_Property (N));
            Check_Simple (Get_Boolean (N));
         when N_Always
           | N_Never
           | N_Eventually
           | N_Strong =>
            Check_Simple (Get_Property (N));
         when N_Braced_SERE =>
            Check_Simple (Get_SERE (N));
         when N_Concat_SERE
           | N_Fusion_SERE
           | N_Within_SERE =>
            Check_Simple (Get_Left (N));
            Check_Simple (Get_Right (N));
         when N_Name =>
            null;
         when N_Star_Repeat_Seq
           | N_Goto_Repeat_Seq
           | N_Equal_Repeat_Seq =>
            declare
               N2 : constant Node := Get_Sequence (N);
            begin
               if N2 /= Null_Node then
                  Check_Simple (N2);
               end if;
            end;
         when N_Plus_Repeat_Seq =>
            Check_Simple (Get_Sequence (N));
         when N_Match_And_Seq
           | N_And_Seq
           | N_Or_Seq =>
            Check_Simple (Get_Left (N));
            Check_Simple (Get_Right (N));
         when N_Imp_Seq
           | N_Overlap_Imp_Seq =>
            Check_Simple (Get_Sequence (N));
            Check_Simple (Get_Property (N));
         when N_Log_Imp_Prop
           | N_Until
           | N_Before
           | N_Or_Prop
           | N_And_Prop
           | N_And_Bool
           | N_Or_Bool
           | N_Imp_Bool =>
            Check_Simple (Get_Left (N));
            Check_Simple (Get_Right (N));
         when N_Next
           | N_Next_A
           | N_Next_E =>
            Check_Simple (Get_Property (N));
         when N_Next_Event
           | N_Next_Event_A
           | N_Next_Event_E
           | N_Abort =>
            Check_Simple (Get_Boolean (N));
            Check_Simple (Get_Property (N));
         when N_Not_Bool =>
            Check_Simple (Get_Boolean (N));
         when N_Const_Parameter
           | N_Sequence_Parameter
           | N_Boolean_Parameter
           | N_Property_Parameter =>
            null;
         when N_Actual =>
            null;
         when N_Sequence_Instance
           | N_Endpoint_Instance
           | N_Property_Instance =>
            null;
         when N_True
           | N_False
           | N_Number
           | N_EOS
           | N_HDL_Expr =>
            null;
      end case;
   end Check_Simple;
end PSL.Subsets;