Changes between Version 126 and Version 127 of IR2


Ignore:
Timestamp:
06/10/21 08:54:25 (5 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • IR2

    v126 v127  
    123123type-specifier:
    124124    ID type-args?  /* type parameter or (possibly parameterized) typedef use */
    125   | '$int'  /* mathematical integers */
    126   | '$bool'  /* boolean type ($true and $false, unrelated to integers) */
    127   | '$char'  /* character type (Unicode characters, unrelated to integers) */
    128   | '$real'   /* mathematical reals */
    129   | '$float32'  /* IEEE 32-bit floating-point numbers */
    130   | '$float64'  /* IEEE 64-bit floating-point number */
     125  | '$int' size-spec  /* mathematical integers */
     126  | '$bool' size-spec  /* boolean type ($true and $false, unrelated to integers) */
     127  | '$char' size-spec  /* character type (Unicode characters, unrelated to integers) */
     128  | '$real' size-spec   /* mathematical reals */
     129  | '$float' size-spec  /* IEEE floating-point numbers */
    131130  | '$herbrand' '<' type-name '>'  /* Herbrand type of non-Herbrand numeric type T */
    132131  | '$proc'  /* process type */
    … …  
    142141  | '$rel' type-args  /* relation: set of n-tuples with specified component types */
    143142  ;
    144 type-qualifier : '$size' '(' constant-expr ')'   /* size specification (in bytes) */
     143size-spec: '<' expr '>' ;
    145144declarator: '*'* direct-declarator ;
    146145direct-declarator:
    … …  
    165164=== Notes ===
    166165
    167 * Certain basic types can have a specified size---the number of bytes consumed by an object of that type.  These basic types include '$bool', '$int', '$char', and '$real'.   Two versions of the basic type with different sizes are in fact disjoint types.  The basic type without a specified size has domain the union over all sizes of the size-qualified type.
     166* Certain basic types can have a specified size---the number of bytes consumed by an object of that type.  These basic types include '$bool', '$int', '$char', and '$real'.   Two versions of the basic type with different sizes are in fact disjoint types.  The basic type without a specified size has domain the union over all sizes of the size-qualified type.  TODO: require this or option?
    168167* Sequences, sets, maps, relations, and `$mem` objects are immutable.   An assignment using objects of this type creates a new copy of the object, just as with primitive types like `$int`.
    169168* Arrays are similar to sequences.   The main differences are as follows:
    … …  
    259258  | expr type-args? '(' expression-list? ')'  /* application of abstract function (and perhaps other functions?) */
    260259  | '$typeof' '(' type-name ')'  /* value type named by the extended type name */
     260  | 'sizeof' '(' (type-name | expr) ')'  /* C's sizeof expression --- number of bytes */
    261261  | '$fresh' '(' (expr | type-name) ')'  /* returns a new arbitrary value of the given type */
    262262  | '$new' '(' (expr | type-name) ')'  /* returns a new arbitrary and undefined value of the given complete type */
    … …  
    329329=== Allowed Casts ===
    330330
     331* between two types that are the same except for sizes of the basic types
    331332* `$int` -> `$real`
    332 * `$float32` -> `$real`
    333 * `$float64` -> `$real`
     333* `$float` -> `$real`
    334334* `T1*` -> `T2*`.   How to check a cast is valid?  What happens if it is not?  If there are no exceptions, something must be returned.  Perhaps undefined value.
    335335  * this is OK if one is a pointer to element 0 of an array, and the other is a pointer to the array
    … …  
    352352$system void $exit();  // terminate process immediately
    353353$system $bool $terminated($proc p);  // has the process terminated?
    354 $system int $choose_int($int n);  // nondeterministic choice of int in 0..n-1
     354$template <$int s> $system $int<s> $choose_int($int<s> n);  // nondeterministic choice of int in 0..n-1
    355355
    356356}}}
    … …  
    364364could be modeled as
    365365{{{
    366 $int * p;
    367 $int (*p1)[]; // pointer to array of $int
    368 p1 = $alloc(&heap, $new($int[10]));
     366int * p;
     367int (*p1)[]; // pointer to array of int
     368p1 = $alloc(&heap, $new(int[10]));
    369369p = &(*p1)[0];
    370370}}}
    … …  
    391391
    392392{{{
    393 $int $round($real x); // round to nearest integer
    394 $int $floor($real x); // greatest integer less than or equal to
    395 $int $ceil($real x); // least integer greater than or equal to
    396 $float32 $round32($real x, $int mode);  // round to float32 (see modes above)
    397 $float64 $round64($real x, $int mode);  // round to float64 (see modes above)
     393$template <$int s> $int<s> $round($real x); // round to nearest integer
     394$template <$int s> $int<s> $floor($real x); // greatest integer less than or equal to
     395$template <$int s> $int<s> $ceil($real x); // least integer greater than or equal to
     396$template <$int s> $float<s> $roundf($real x, $int mode);  // round to float (see modes above)
    398397$real $abs($real x); // absolute value on reals
    399 $int $absi($int x); // absolute value on integers
    400 $float32 $abs32($float32 x); // absolute value on $float32
     398$template <$int s> $int<s> $absi($int<s> x); // absolute value on integers
     399$template <$int s> $float<s> $absf($float<s> x); // absolute value on $float
     400...left off here...
    401401$float64 $abs64($float64 x); // absolute value on $float64
    402402$real $pow($real x, $int n);  // x to the n-th power.  n>=0