Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Better primitive type support in custom string and numeral notations.
- float and array values are now supported for printing and parsing in custom notations (and in notations defined using the ocaml API) - the three constants bound to the primitive float, int and array type are now allowed anywhere inside a term to print, to handle them similar to `real` type constructors - Grants #13484: String notations for primitive arrays - Fixes #13517: String notation printing fails with primitive integers inside lists
- Loading branch information
Showing
11 changed files
with
216 additions
and
3 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
- **Added:** | ||
:cmd:`Number Notation` and :cmd:`String Notation` now support | ||
parsing and printing of primitive floats, primitive arrays | ||
and type constants of primitive types. | ||
(`#13519 <https://github.com/coq/coq/pull/13519>`_, | ||
fixes `#13484 <https://github.com/coq/coq/issues/13484>`_ | ||
and `#13517 <https://github.com/coq/coq/issues/13517>`_, | ||
by Fabian Kunze, with help of Jason Gross) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
"abc" | ||
: intList | ||
"abc" | ||
: intList | ||
mk_intList [97%int63; 98%int63; 99%int63] | ||
: intList | ||
"abc" | ||
: intArray | ||
"abc" | ||
: intArray | ||
= "abc" | ||
: nestArray | ||
"abc" | ||
: nestArray | ||
"100" | ||
: floatList | ||
"100" | ||
: floatList | ||
mk_floatList [1%float; 0%float; 0%float] | ||
: floatList |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,139 @@ | ||
Require Import Coq.Lists.List. | ||
Require Import Coq.Strings.String Coq.Strings.Byte Coq.Strings.Ascii. | ||
Require Coq.Array.PArray Coq.Floats.PrimFloat. | ||
Require Import Coq.Numbers.BinNums Coq.Numbers.Cyclic.Int63.Int63. | ||
|
||
Set Printing Depth 100000. | ||
Set Printing Width 1000. | ||
|
||
Close Scope char_scope. | ||
Close Scope string_scope. | ||
|
||
(* Notations for primitive integers inside polymorphic datatypes *) | ||
Module Test1. | ||
Inductive intList := mk_intList (_ : list int). | ||
Definition i63_from_byte (b : byte) : int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)). | ||
Definition i63_to_byte (i : int) : byte := | ||
match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end. | ||
|
||
Definition to_byte_list '(mk_intList a) := List.map i63_to_byte a. | ||
|
||
Definition from_byte_list (xs : list byte) : intList:= | ||
mk_intList (List.map i63_from_byte xs). | ||
|
||
Declare Scope intList_scope. | ||
Delimit Scope intList_scope with intList. | ||
|
||
String Notation intList from_byte_list to_byte_list : intList_scope. | ||
|
||
Open Scope intList_scope. | ||
Import List.ListNotations. | ||
Check mk_intList [97; 98; 99]%int63%list. | ||
Check "abc"%intList. | ||
|
||
Definition int' := int. | ||
Check mk_intList (@cons int' 97 [98; 99])%int63%list. | ||
End Test1. | ||
|
||
Import PArray. | ||
|
||
(* Notations for primitive arrays *) | ||
Module Test2. | ||
Inductive intArray := mk_intArray (_ : array int). | ||
|
||
Definition i63_from_byte (b : byte) : Int63.int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)). | ||
Definition i63_to_byte (i : Int63.int) : byte := | ||
match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end. | ||
|
||
Definition i63_to_nat x := BinInt.Z.to_nat (Int63.to_Z x). | ||
Local Definition nat_length {X} (x : array X) :nat := i63_to_nat (length x). | ||
|
||
Local Fixpoint list_length_i63 {A} (xs : list A) :int := | ||
match xs with | ||
| nil => 0 | ||
| cons _ xs => 1 + list_length_i63 xs | ||
end. | ||
|
||
Definition to_byte_list '(mk_intArray a) := | ||
((fix go (n : nat) (i : Int63.int) (acc : list byte) := | ||
match n with | ||
| 0 => acc | ||
| S n => go n (i - 1) (cons (i63_to_byte a.[i]) acc) | ||
end) (nat_length a) (length a - 1) nil)%int63. | ||
|
||
Definition from_byte_list (xs : list byte) := | ||
(let arr := make (list_length_i63 xs) 0 in | ||
mk_intArray ((fix go i xs acc := | ||
match xs with | ||
| nil => acc | ||
| cons x xs => go (i + 1) xs (acc.[i <- i63_from_byte x]) | ||
end) 0 xs arr))%int63. | ||
|
||
Declare Scope intArray_scope. | ||
Delimit Scope intArray_scope with intArray. | ||
|
||
String Notation intArray from_byte_list to_byte_list : intArray_scope. | ||
|
||
Open Scope intArray_scope. | ||
Check mk_intArray ( [| 97; 98; 99 | 0|])%int63%array. | ||
Check "abc"%intArray. | ||
|
||
End Test2. | ||
|
||
(* Primitive arrays inside primitive arrays *) | ||
Module Test3. | ||
|
||
Inductive nestArray := mk_nestArray (_ : array (array int)). | ||
Definition to_byte_list '(mk_nestArray a) := | ||
((fix go (n : nat) (i : Int63.int) (acc : list byte) := | ||
match n with | ||
| 0 => acc | ||
| S n => go n (i - 1) (cons (Test2.i63_to_byte a.[i].[0]) acc) | ||
end) (Test2.nat_length a) (length a - 1) nil)%int63. | ||
|
||
Definition from_byte_list (xs : list byte) := | ||
(let arr := make (Test2.list_length_i63 xs) (make 0 0) in | ||
mk_nestArray ((fix go i xs acc := | ||
match xs with | ||
| nil => acc | ||
| cons x xs => go (i + 1) xs (acc.[i <- make 1 (Test2.i63_from_byte x)]) | ||
end) 0 xs arr))%int63. | ||
|
||
Declare Scope nestArray_scope. | ||
Delimit Scope nestArray_scope with nestArray. | ||
|
||
String Notation nestArray from_byte_list to_byte_list : nestArray_scope. | ||
|
||
Open Scope nestArray_scope. | ||
Eval cbv in mk_nestArray ( [| make 1 97; make 1 98; make 1 99 | make 0 0|])%int63%array. | ||
Check "abc"%nestArray. | ||
End Test3. | ||
|
||
|
||
|
||
(* Notations for primitive floats inside polymorphic datatypes *) | ||
Module Test4. | ||
Import PrimFloat. | ||
Inductive floatList := mk_floatList (_ : list float). | ||
Definition float_from_byte (b : byte) : float := | ||
if Byte.eqb b "0"%byte then PrimFloat.zero else PrimFloat.one. | ||
Definition float_to_byte (f : float) : byte := | ||
if PrimFloat.is_zero f then "0" else "1". | ||
Definition to_byte_list '(mk_floatList a) := List.map float_to_byte a. | ||
|
||
Definition from_byte_list (xs : list byte) : floatList:= | ||
mk_floatList (List.map float_from_byte xs). | ||
|
||
Declare Scope floatList_scope. | ||
Delimit Scope floatList_scope with floatList. | ||
|
||
String Notation floatList from_byte_list to_byte_list : floatList_scope. | ||
|
||
Open Scope floatList_scope. | ||
Import List.ListNotations. | ||
Check mk_floatList [97; 0; 0]%float%list. | ||
Check "100"%floatList. | ||
|
||
Definition float' := float. | ||
Check mk_floatList (@cons float' 1 [0; 0])%float%list. | ||
End Test4. |