Ignore:
Timestamp:
Mar 31, 2011, 5:20:00 PM (9 years ago)
Author:
campbell
Message:

Enough fixes to let an RTLabs program run.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r702 r727  
    4040  | Ointuoffloat: unary_operation          (**r unsigned integer to float *)
    4141  | Ofloatofint: unary_operation           (**r float to signed integer *)
    42   | Ofloatofintu: unary_operation.         (**r float to unsigned integer *)
     42  | Ofloatofintu: unary_operation          (**r float to unsigned integer *)
     43  | Oid: unary_operation                   (**r identity (used to move between registers *)
     44  | Optrofint: region → unary_operation    (**r int to pointer with given representation *)
     45  | Ointofptr: unary_operation.            (**r pointer to int *)
    4346
    4447inductive binary_operation : Type[0] ≝
     
    6265  | Ocmp: comparison -> binary_operation   (**r integer signed comparison *)
    6366  | Ocmpu: comparison -> binary_operation  (**r integer unsigned comparison *)
    64   | Ocmpf: comparison -> binary_operation. (**r float comparison *)
     67  | Ocmpf: comparison -> binary_operation  (**r float comparison *)
     68  | Oaddp: binary_operation                (**r add an integer to a pointer *)
     69  | Osubp: binary_operation                (**r subtract two pointers *)
     70  | Ocmpp: comparison → binary_operation.  (**r compare pointers *)
    6571
    6672
     
    105111  | Ofloatofint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofint n1)) | _ ⇒ None ? ]
    106112  | Ofloatofintu ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofintu n1)) | _ ⇒ None ? ]
     113  | Oid ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
     114  (* Only conversion of null pointers is specified. *)
     115  | Optrofint r ⇒ match arg with [ Vint n1 ⇒ if eq n1 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
     116  | Ointofptr ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
    107117  ].
    108118
     
    445455  | Ocmpu c ⇒ ev_cmpu c
    446456  | Ocmpf c ⇒ ev_cmpf c
    447   ].
    448 
     457  (* FIXME: it doesn't make sense to use the same operation for ints and ptrs. *)
     458  | Oaddp ⇒ ev_add
     459  | Osubp ⇒ ev_sub
     460  | Ocmpp c ⇒ ev_cmp c
     461  ].
     462
Note: See TracChangeset for help on using the changeset viewer.