Re: Ada 2012 Constraints (WRT an Ada IR)

[Shark8 <onewingedshark@gmail.com>]

On Wednesday, November 30, 2016 at 1:31:17 AM UTC-7, Dmitry A. Kazakov wrote:
> 
> BTW, "representing" is certainly irrelevant because Ada is a statically 
> typed language, hence, no types are ever represented in an Ada program 
> [they are in the compiler and then the representations are thrown away].

Insofar as you can think of the Ada translator as a function of the form "Function Translate( Input : Source ) Return Executable_or_Library_Object;" that's absolutely true... it is untrue if you are considering an IR (intermediate representation).

Now we could decompose Translate along the phases of compilation as something perhaps like:

    Function Translate( Input : Source ) Return Executable_or_Library_Object is
    ( Code_Generator(Optimizer(Semantic_Analyzer((Parser((Lexer(Source))))))) );

and, further, if we were to instead do something like this:

    Function Translate( Input : Source ) Return Executable_or_Library_Object is
    Begin
      declare
        Semantic_Tree : constant Semantic_Analysis_Result := 
            Semantic_Analyzer(Parser(Lexer(Source)));
      begin
        Semantic_Analysis_Result'Write( IR_Stream, Semantic_Tree );
        Return Code_Generator(Optimizer(Semantic_Tree));
      end;
    End Translate;

The result would be that the compiler phases 'Lexer' through 'Semantic_Analyzer' have been "captured" into the stream IR_Stream, and it's guaranteed to be valid Ada (insofar as the correctness of the implementation of those phases are concerned) and, moreover, consistent w/ itself. We could then at a later date read that stream into a Semantic_Analysis_Result object and continue the compilation process (optimizing and code-gen). -- So, with that in mind it makes sense to consider the usefulness of making Semantic_Analysis_Result its own formal language: the Intermediate Representation.

Because of the properties listed above, every instance of Semantic_Analysis_Result is valid, consistent Ada -- by uniformly representing the underlying construct/concepts of the Ada-source we can severely cut down the complexity needed by the later stages of the compiler^1  (like, say, the DER encodings vs the BER encodings of ASN.1).

These properties are ideal for many applications -- one of the most practical to addressing some of the complaints/difficulties leveled at Ada (like a poor ecosystem) would be implementation of a CPAN-style repository... but far better -- for if we can, say, make this IR amiable to storage in a DB (with attendant consistency-checks) we can eliminate the storage of invalid Ada in said repository; furthermore, because we have all the semantic-information already we could build-in tools to allow correct dependency-storage, like Gnoga using Simple Components, but with proper versioning so that a breaking change in a new version's API could be detected and the older one with the required properties could be retrieved.

> On 29/11/2016 23:59, Shark8 wrote:
> > On Tuesday, November 29, 2016 at 2:06:21 PM UTC-7, Dmitry A. Kazakov wrote:
> >> On 2016-11-29 21:51, Shark8 wrote:
> >>> On Tuesday, November 29, 2016 at 1:44:43 PM UTC-7, Dmitry A. Kazakov wrote:
> >>>> On 2016-11-29 21:32, Shark8 wrote:
> >>>>
> >>>>> The above has a constraint -- that of only holding digits -- but
> >>>>> still  is unconstrained. If we were doing a formal CS class we'd say something
> >>>>> like "The type Serial_Number contains all strings that have only the
> >>>>> decimal digits therein."
> >>>>
> >>>> You want convariance, that is a completely different beast.
> >>>
> >>> No, I really don't.
> >>> I'm not talking about Ada-syntax,
> >>
> >> Yes you do, covariance vs. contravariance is semantics, not syntax.
> >
> > Maybe I'm misunderstanding.
> > I simply don't see how covariance vs. contravariance is at all
> > germane  to representing the definition of a type.
> 
> It is relevant to the difference between Ada 83 style constrained types 
> and constrained types introduced by predicates. Ada 83 constraints are 
> more consistent because they took into account operations that must be 
> covariant. E.g. adding to the list of examples:
> 
>     subtype Text is String (1..80);
> 
> That overrides 'First, 'Last, 'Range, 'Length and propagates the 
> constraint to other types by promoting Text definite. None of this 
> happens if you add a predicate because all operations are inherited 
> as-is = contravariant.

And shouldn't that (eg Predicated_Subtype'Pred or 'Last, etc) be caught by the semantic-analysis phase? If so, then it's entirely a moot point, isn't it?

But it certainly doesn't invalidate the concept of considering a type [and subtype] as the collection of a set of values and a set of operations on those values; for example:

    Type Nybble is range 0..15 with Size => 4;
    Subtype Prime_Nybble is Nybble with
      Static_Predicate => Prime_Nybble in 2|3|5|7|11|13;

could be represented as something which visualized-as-text would be:

   Nybble is
    Size            : Bits(4)
    Internal_Values : Set(0..15)
    Offset          : 0          -- So we could represent 1..16 w/ 4-bits
    Operations      : Arithmetic_ops & Scalar_Attributes

   
   Prime_Nybble modifying Nybble is
    Operations      : Operations without Scalar_Attributes

or somesuch.

> >>>> It is a new
> >>>> type with some operations overridden, e.g. the operation that yields a
> >>>> value of a discrete type for case statement. It is an implicit operation
> >>>> in Ada, yet it is an operation. It must be covariant, i.e. returning the
> >>>> new type rather than the old one for the case be satisfied with the new
> >>>> set of values. Same with already mentioned 'First, 'Last, 'Range. Or,
> >>>> for that matter, 'Succ and 'Pred if the new type has a non-contiguous
> >>>> values set, e.g. Odd_Number. You cannot get there by merely putting some
> >>>> predicate on the assignment operation (which Ada's predicates do). That
> >>>> model is too weak to express such things.
> >>>
> >>> This is not about defining a type in Ada, it's about abstracting the
> >>> making of a type [in Ada] and how best to represent _that_.
> >>
> >> What is abstracting making the type?
> >
> > Perhaps I should have used the word "defining" or "representing" instead of "making".
> 
> So it *is* about "defining" now?
> 
> [I still do not understand what you meant.]

In some sense, yes. -- By making the IR a mapping of Ada's concepts (such as defining a new type, or adding constraints thereon, [ie] the particular subject of this thread) in a general manner we can simplify some complexity of the Ada language insofar as [implementations of] tools and the back-end of compilers are concerned.

But as a whole, no -- the IR is about (a) abstracting the concepts that underlay Ada, and (b) storing/transforming an Ada text-source in terms of those concepts.

Does that clear things up?

--------------------------------------

^1 -- As an example the Standard says that a renaming of a function-call and a constant-object initialized to that function-call are equivalent; it is therefore quite sensible to have a single IR-construct to represent both... if exact source-text recovery is important then simply adding a discriminant/field of "Is_Renaming : Boolean" would be enough to track source recovery for that construct.