• Clément Fumex's avatar
    Add the ability to · f0547868
    Clément Fumex authored
    * declare range types and float types,
    * use integer (resp. real) literals for those types through casting,
    * specify how to print them in drivers.
    
    Change in syntax
    * use
    
      type t = < range 1 2 >   (* integers from 1 to 2 *)
      type t' = < float 4 12 > (* float with 4 bits in exponent and 12 in mantissa *)
    
      the two projections :
      t'int
      t''real
    
      and the predicate :
      t''isFinite
    
    * Restrict the use of "'" in whyml:
      Users are not allowed to introduce names where a quote symbol
      is followed by a letter. Thus, the following identifiers are
      valid:
    
      t'
      toto'0''
      toto'_phi
    
      whereas toto'phi is not.
    
    Note: we do not yet support negative numbers in range declaration
    and casting of a literal.
    f0547868
alt_ergo_common.drv 5.25 KB