Changes between Version 25 and Version 26 of IR


Ignore:
Timestamp:
11/22/15 20:39:32 (10 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • IR

    v25 v26  
    5656The types are:
    5757
    58 * `$dytype` : dynamic type: a value of this type represents a "dynamic type", a type which is created at runtime.  For example when the type name `int[n]` is evaluated, the result is a value of type `$dytype`.
     58* `$type` : dynamic type.  This allows a type to be realized as a value, a value of type `$type`.  For example, when the type name `int[n]` is evaluated, the result is a value of type `$type`.
    5959* `$bool` : boolean type, values are `$true` and `$false`
    6060* `$proc` : process type
     
    9191Type names:
    9292
    93 A type name is a syntactic element that names a type, together with possibly more information that makes the type "complete".  All of the names listed above are type names, such as `int[]`, but so is `int[n*m]`.
    94 
    95 The expression `$dytypeof(typeName)` takes a type name and returns a value of type `$dytype` representing that type.
    96 
    97 The expression `$init_val(d)` takes a `$dytype` value `d` and returns the initial value for an object of type `d`.
     93A type name is a syntactic element that names a type, together with possibly more information that makes the type "complete".  All of the names listed above are type names, such as `int[]`, but so is `int[n*m]`.  This is the same as in C.
     94
     95The expression `$typeof(T)`, where `T` is a type name, returns a value of type `$type` representing the type `T`.
     96
     97The expression `$initval(d)` takes a `$type` value `d` and returns the initial value for an object of type `d`.
    9898
    9999Example:
     
    104104// variable decls
    105105int n;
    106 $dytype _S;
     106$type _S;
    107107struct S x1;
    108108struct S x2;
     
    110110// statements (leaving out the chooses and whens for brevity)
    111111n=10;
    112 _S=$dytypeof(struct S { int a[n]; };
    113 x1=$init_val(_S);
     112_S=$typeof(struct S { int a[n]; };
     113x1=$initval(_S);
    114114n=20;
    115 x2=$init_val(_S);
     115x2=$initval(_S);
    116116}}}
    117117
     
    172172 * `NULL` : value of type `void*`
    173173* variables
    174 * `$dytypeof(T)` : an expression of type `$dytype`
    175 * `$init_val(e)`, where `e1` is an expression of type `$dytype`
     174* `$typeof(T)` : an expression of type `$type`
     175* `sizeof(T)` : the size of the type named `T`
     176* `$initval(e)`, where `e` is an expression of type `$type`
    176177* `$defined(e)`
    177178* `e1+e2` : addition
     
    194195* `$forall`, `$exists`
    195196* `e1.i`, some natural number i (tuple read)
    196 * `sizeof(T)` : T is a type name?
    197197* `e1&e2`, `e1|e2`, `e1^e2`, `~e1` : bit-wise operations: arguments are arrays of booleans
    198198* **MemoryUnitExpressions?**: are these literal values of type `$mem`?
     
    244244
    245245== Libraries ==
     246