diff options
| author | Maxime Dénès | 2018-02-16 01:02:17 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2019-02-04 13:12:40 +0000 |
| commit | e43b1768d0f8399f426b92f4dfe31955daceb1a4 (patch) | |
| tree | d46d10f8893205750e7238e69512736243315ef6 /test-suite/success | |
| parent | a1b7f53a68c9ccae637f2c357fbe50a09e211a4a (diff) | |
Primitive integers
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/Compat88.v | 4 | ||||
| -rw-r--r-- | test-suite/success/NumeralNotations.v | 11 |
2 files changed, 13 insertions, 2 deletions
diff --git a/test-suite/success/Compat88.v b/test-suite/success/Compat88.v index e2045900d5..1233a4b8f5 100644 --- a/test-suite/success/Compat88.v +++ b/test-suite/success/Compat88.v @@ -4,7 +4,7 @@ Require Coq.Strings.Ascii Coq.Strings.String. Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef. Require Coq.Reals.Rdefinitions. -Require Coq.Numbers.Cyclic.Int31.Cyclic31. +Require Coq.Numbers.Cyclic.Int63.Cyclic63. Require Import Coq.Compat.Coq88. (* XXX FIXME Should not need [Require], see https://github.com/coq/coq/issues/8311 *) @@ -15,4 +15,4 @@ Check BinNat.N.eqb 1 1. Check BinInt.Z.eqb 1 1. Check BinPos.Pos.eqb 1 1. Check Rdefinitions.Rplus 1 1. -Check Int31.iszero 1. +Check Int63.is_zero 1. diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v index 47ef381270..7b857c70c5 100644 --- a/test-suite/success/NumeralNotations.v +++ b/test-suite/success/NumeralNotations.v @@ -300,3 +300,14 @@ Module Test16. (** Ideally this should work, but it should definitely not anomaly *) Fail Check let v := 0%test16 in v : Foo. End Test16. + +Require Import Coq.Numbers.Cyclic.Int63.Int63. +Module Test17. + (** Test int63 *) + Declare Scope test17_scope. + Delimit Scope test17_scope with test17. + Local Set Primitive Projections. + Record myint63 := of_int { to_int : int }. + Numeral Notation myint63 of_int to_int : test17_scope. + Check let v := 0%test17 in v : myint63. +End Test17. |