diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 3fdb67e900..cc56751d77 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -342,6 +342,32 @@ Definition to_num_int n := Number.IntDecimal (to_int n). Definition to_num_hex_int n := Number.IntHexadecimal (to_hex_int n). +(** ** Little-endian conversions (least significant digit first) *) + +Definition of_luint (d:Decimal.luint) := Pos.of_luint d. +Definition of_hex_luint (d:Hexadecimal.luint) := Pos.of_hex_luint d. + +Definition of_num_luint (d:Number.luint) := + match d with + | Number.LUIntDecimal d => of_luint d + | Number.LUIntHexadecimal d => of_hex_luint d + end. + +Definition to_luint n := + match n with + | 0 => {| Decimal.luint_IsLittleEndian := Decimal.zero |} + | pos p => Pos.to_luint p + end. + +Definition to_hex_luint n := + match n with + | 0 => {| Hexadecimal.luint_IsLittleEndian := Hexadecimal.zero |} + | pos p => Pos.to_hex_luint p + end. + +Definition to_num_luint n := Number.LUIntDecimal (to_luint n). +Definition to_num_hex_luint n := Number.LUIntHexadecimal (to_hex_luint n). + Number Notation N of_num_uint to_num_hex_uint : hex_N_scope. Number Notation N of_num_uint to_num_uint : N_scope. diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 9a4ad9a4c2..a8a68ed9db 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -375,6 +375,56 @@ Definition to_num_int n := Number.IntDecimal (to_int n). Definition to_num_hex_int n := Number.IntHexadecimal (to_hex_int n). +(** ** Little-endian conversions (least significant digit first) *) + +Definition of_luint (d:Decimal.luint) := + of_uint (Decimal.rev (Decimal.luint_IsLittleEndian d)). + +Definition of_hex_luint (d:Hexadecimal.luint) := + of_hex_uint (Hexadecimal.rev (Hexadecimal.luint_IsLittleEndian d)). + +Definition of_num_luint (d:Number.luint) : N := + match d with + | Number.LUIntDecimal d => of_luint d + | Number.LUIntHexadecimal d => of_hex_luint d + end. + +Definition of_lint (d:Decimal.lint) : option positive := + of_int (match Decimal.lint_IsLittleEndian d with + | Decimal.Pos u => Decimal.Pos (Decimal.rev u) + | Decimal.Neg u => Decimal.Neg (Decimal.rev u) + end). + +Definition of_hex_lint (d:Hexadecimal.lint) : option positive := + of_hex_int (match Hexadecimal.lint_IsLittleEndian d with + | Hexadecimal.Pos u => Hexadecimal.Pos (Hexadecimal.rev u) + | Hexadecimal.Neg u => Hexadecimal.Neg (Hexadecimal.rev u) + end). + +Definition of_num_lint (d:Number.lint) : option positive := + match d with + | Number.LIntDecimal d => of_lint d + | Number.LIntHexadecimal d => of_hex_lint d + end. + +Definition to_luint p := + {| Decimal.luint_IsLittleEndian := to_little_uint p |}. + +Definition to_hex_luint p := + {| Hexadecimal.luint_IsLittleEndian := to_little_hex_uint p |}. + +Definition to_num_luint p := Number.LUIntDecimal (to_luint p). +Definition to_num_hex_luint p := Number.LUIntHexadecimal (to_hex_luint p). + +Definition to_lint n := + {| Decimal.lint_IsLittleEndian := Decimal.Pos (to_little_uint n) |}. + +Definition to_hex_lint p := + {| Hexadecimal.lint_IsLittleEndian := Hexadecimal.Pos (to_little_hex_uint p) |}. + +Definition to_num_lint n := Number.LIntDecimal (to_lint n). +Definition to_num_hex_lint n := Number.LIntHexadecimal (to_hex_lint n). + Number Notation positive of_num_int to_num_hex_uint : hex_positive_scope. Number Notation positive of_num_int to_num_uint : positive_scope. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index db887f0c74..6367e707c4 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -304,6 +304,48 @@ Definition ldiff a b := | neg a, neg b => of_N (N.ldiff (Pos.pred_N b) (Pos.pred_N a)) end. +(** ** Little-endian conversions (least significant digit first) *) + +Definition of_luint (d:Decimal.luint) := of_N (Pos.of_luint d). +Definition of_hex_luint (d:Hexadecimal.luint) := of_N (Pos.of_hex_luint d). + +Definition of_lint (d:Decimal.lint) := + of_int (match Decimal.lint_IsLittleEndian d with + | Decimal.Pos u => Decimal.Pos (Decimal.rev u) + | Decimal.Neg u => Decimal.Neg (Decimal.rev u) + end). + +Definition of_hex_lint (d:Hexadecimal.lint) := + of_hex_int (match Hexadecimal.lint_IsLittleEndian d with + | Hexadecimal.Pos u => Hexadecimal.Pos (Hexadecimal.rev u) + | Hexadecimal.Neg u => Hexadecimal.Neg (Hexadecimal.rev u) + end). + +Definition of_num_lint (d:Number.lint) := + match d with + | Number.LIntDecimal d => of_lint d + | Number.LIntHexadecimal d => of_hex_lint d + end. + +Definition to_lint n := + {| Decimal.lint_IsLittleEndian := + match n with + | 0 => Decimal.Pos Decimal.zero + | pos p => Decimal.Pos (Pos.to_little_uint p) + | neg p => Decimal.Neg (Pos.to_little_uint p) + end |}. + +Definition to_hex_lint n := + {| Hexadecimal.lint_IsLittleEndian := + match n with + | 0 => Hexadecimal.Pos Hexadecimal.zero + | pos p => Hexadecimal.Pos (Pos.to_little_hex_uint p) + | neg p => Hexadecimal.Neg (Pos.to_little_hex_uint p) + end |}. + +Definition to_num_lint n := Number.LIntDecimal (to_lint n). +Definition to_num_hex_lint n := Number.LIntHexadecimal (to_hex_lint n). + Number Notation Z of_num_int to_num_hex_int : hex_Z_scope. Number Notation Z of_num_int to_num_int : Z_scope.