diff options
Diffstat (limited to 'mppa_k1c/SelectLong.vp')
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 26735c99..a3aefb15 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -341,20 +341,29 @@ Definition floatoflongu (e: expr) := if Archi.splitlong then SplitLong.floatoflongu e else Eop Ofloatoflongu (e:::Enil). -Definition longofsingle (e: expr) := +(* FIXME - normally we can have it natively, but in practice it requires proving that we can do Fwidenlwd + fixedd.rz.. To do later *) +Definition longofsingle (e: expr) := SplitLong.longofsingle e. +(* if Archi.splitlong then SplitLong.longofsingle e else Eop Olongofsingle (e:::Enil). +*) -Definition longuofsingle (e: expr) := +Definition longuofsingle (e: expr) := SplitLong.longuofsingle e. +(* if Archi.splitlong then SplitLong.longuofsingle e else Eop Olonguofsingle (e:::Enil). +*) -Definition singleoflong (e: expr) := +Definition singleoflong (e: expr) := SplitLong.singleoflong e. +(* if Archi.splitlong then SplitLong.singleoflong e else Eop Osingleoflong (e:::Enil). +*) -Definition singleoflongu (e: expr) := +Definition singleoflongu (e: expr) := SplitLong.singleoflongu e. +(* if Archi.splitlong then SplitLong.singleoflongu e else Eop Osingleoflongu (e:::Enil). +*) End SELECT. |