aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/bug_12257.v3
-rw-r--r--test-suite/output/Extraction_Haskell_String_12258.out73
-rw-r--r--test-suite/output/Extraction_Haskell_String_12258.v52
-rw-r--r--test-suite/output/Fixpoint.out24
-rw-r--r--test-suite/output/Fixpoint.v38
-rw-r--r--test-suite/output/bug_12159.out28
-rw-r--r--test-suite/output/bug_12159.v39
-rw-r--r--test-suite/ssr/simpl_done.v28
-rw-r--r--test-suite/ssr/try_case.v11
9 files changed, 293 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/bug_12257.v b/test-suite/bugs/closed/bug_12257.v
new file mode 100644
index 0000000000..4962048a42
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12257.v
@@ -0,0 +1,3 @@
+(* Test that ExtrHaskellString transitively requires ExtrHaskellBasic *)
+Require Coq.extraction.ExtrHaskellString.
+Import Coq.extraction.ExtrHaskellBasic.
diff --git a/test-suite/output/Extraction_Haskell_String_12258.out b/test-suite/output/Extraction_Haskell_String_12258.out
new file mode 100644
index 0000000000..615abaa3e8
--- /dev/null
+++ b/test-suite/output/Extraction_Haskell_String_12258.out
@@ -0,0 +1,73 @@
+{-# OPTIONS_GHC -cpp -XMagicHash #-}
+{- For Hugs, use the option -F"cpp -P -traditional" -}
+
+{- IMPORTANT: If you change this file, make sure that running [cp
+ Extraction_Haskell_String_12258.out Extraction_Haskell_String_12258.hs &&
+ ghc -o test Extraction_Haskell_String_12258.hs] succeeds -}
+
+module Main where
+
+import qualified Prelude
+
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base
+#else
+-- HUGS
+import qualified IOExts
+#endif
+
+#ifdef __GLASGOW_HASKELL__
+unsafeCoerce :: a -> b
+unsafeCoerce = GHC.Base.unsafeCoerce#
+#else
+-- HUGS
+unsafeCoerce :: a -> b
+unsafeCoerce = IOExts.unsafeCoerce
+#endif
+
+#ifdef __GLASGOW_HASKELL__
+type Any = GHC.Base.Any
+#else
+-- HUGS
+type Any = ()
+#endif
+
+data Output_type_code =
+ Ascii_dec
+ | Ascii_eqb
+ | String_dec
+ | String_eqb
+ | Byte_eqb
+ | Byte_eq_dec
+
+type Output_type = Any
+
+output :: Output_type_code -> Output_type
+output c =
+ case c of {
+ Ascii_dec ->
+ unsafeCoerce
+ ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool);
+ Ascii_eqb ->
+ unsafeCoerce
+ ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool);
+ String_dec ->
+ unsafeCoerce
+ ((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool);
+ String_eqb ->
+ unsafeCoerce
+ ((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool);
+ Byte_eqb ->
+ unsafeCoerce
+ ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool);
+ Byte_eq_dec ->
+ unsafeCoerce
+ ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool)}
+
+type Coq__IO a = GHC.Base.IO a
+
+main :: GHC.Base.IO ()
+main =
+ ((Prelude.>>=) (GHC.Base.return output) (\_ -> GHC.Base.return ()))
+
+
diff --git a/test-suite/output/Extraction_Haskell_String_12258.v b/test-suite/output/Extraction_Haskell_String_12258.v
new file mode 100644
index 0000000000..063ff64337
--- /dev/null
+++ b/test-suite/output/Extraction_Haskell_String_12258.v
@@ -0,0 +1,52 @@
+Require Import Coq.extraction.Extraction.
+Require Import Coq.extraction.ExtrHaskellString.
+Extraction Language Haskell.
+Set Extraction File Comment "IMPORTANT: If you change this file, make sure that running [cp Extraction_Haskell_String_12258.out Extraction_Haskell_String_12258.hs && ghc -o test Extraction_Haskell_String_12258.hs] succeeds".
+Inductive output_type_code :=
+| ascii_dec
+| ascii_eqb
+| string_dec
+| string_eqb
+| byte_eqb
+| byte_eq_dec
+.
+
+Definition output_type_sig (c : output_type_code) : { T : Type & T }
+ := existT (fun T => T)
+ _
+ match c return match c with ascii_dec => _ | _ => _ end with
+ | ascii_dec => Ascii.ascii_dec
+ | ascii_eqb => Ascii.eqb
+ | string_dec => String.string_dec
+ | string_eqb => String.eqb
+ | byte_eqb => Byte.eqb
+ | byte_eq_dec => Byte.byte_eq_dec
+ end.
+
+Definition output_type (c : output_type_code)
+ := Eval cbv [output_type_sig projT1 projT2] in
+ projT1 (output_type_sig c).
+Definition output (c : output_type_code) : output_type c
+ := Eval cbv [output_type_sig projT1 projT2] in
+ match c return output_type c with
+ | ascii_dec as c
+ | _ as c
+ => projT2 (output_type_sig c)
+ end.
+
+Axiom IO_unit : Set.
+Axiom _IO : Set -> Set.
+Axiom _IO_bind : forall {A B}, _IO A -> (A -> _IO B) -> _IO B.
+Axiom _IO_return : forall {A : Set}, A -> _IO A.
+Axiom cast_io : _IO unit -> IO_unit.
+Extract Constant _IO "a" => "GHC.Base.IO a".
+Extract Inlined Constant _IO_bind => "(Prelude.>>=)".
+Extract Inlined Constant _IO_return => "GHC.Base.return".
+Extract Inlined Constant IO_unit => "GHC.Base.IO ()".
+Extract Inlined Constant cast_io => "".
+
+Definition main : IO_unit
+ := cast_io (_IO_bind (_IO_return output)
+ (fun _ => _IO_return tt)).
+
+Recursive Extraction main.
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index 60bc9cbf55..ff7918b4e6 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -12,3 +12,27 @@ let fix f (m : nat) : nat := match m with
Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1)
= cofix inf : Inf := {| projS := inf |}
: Inf
+File "stdin", line 57, characters 0-51:
+Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints]
+File "stdin", line 60, characters 0-103:
+Warning: Not a fully mutually defined fixpoint
+(k1 depends on k2 but not conversely).
+Well-foundedness check may fail unexpectedly.
+ [non-full-mutual,fixpoints]
+File "stdin", line 62, characters 0-106:
+Warning: Not a fully mutually defined fixpoint
+(l2 and l1 are not mutually dependent).
+Well-foundedness check may fail unexpectedly.
+ [non-full-mutual,fixpoints]
+File "stdin", line 64, characters 0-103:
+Warning: Not a fully mutually defined fixpoint
+(m2 and m1 are not mutually dependent).
+Well-foundedness check may fail unexpectedly.
+ [non-full-mutual,fixpoints]
+File "stdin", line 72, characters 0-25:
+Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints]
+File "stdin", line 75, characters 0-48:
+Warning: Not a fully mutually defined fixpoint
+(a2 and a1 are not mutually dependent).
+Well-foundedness check may fail unexpectedly.
+ [non-full-mutual,fixpoints]
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index 398528de72..26c276b68b 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -44,7 +44,39 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
lia.
Qed.
-CoInductive Inf := S { projS : Inf }.
-Definition expand_Inf (x : Inf) := S (projS x).
-CoFixpoint inf := S inf.
+CoInductive Inf := IS { projS : Inf }.
+Definition expand_Inf (x : Inf) := IS (projS x).
+CoFixpoint inf := IS inf.
Eval compute in inf.
+
+Module Recursivity.
+
+Open Scope nat_scope.
+
+Fixpoint f n := match n with 0 => 0 | S n => f n end.
+Fixpoint g n := match n with 0 => 0 | S n => n end.
+Fixpoint h1 n := match n with 0 => 0 | S n => h2 n end
+with h2 n := match n with 0 => 0 | S n => h1 n end.
+Fixpoint k1 n := match n with 0 => 0 | S n => k2 n end
+with k2 n := match n with 0 => 0 | S n => n end.
+Fixpoint l1 n := match n with 0 => 0 | S n => l1 n end
+with l2 n := match n with 0 => 0 | S n => l2 n end.
+Fixpoint m1 n := match n with 0 => 0 | S n => m1 n end
+with m2 n := match n with 0 => 0 | S n => n end.
+(* Why not to allow this definition ?
+Fixpoint h1' n := match n with 0 => 0 | S n => h2' n end
+with h2' n := h1' n.
+*)
+CoInductive S := cons : nat -> S -> S.
+CoFixpoint c := cons 0 c.
+CoFixpoint d := cons 0 c.
+CoFixpoint e1 := cons 0 e2
+with e2 := cons 1 e1.
+CoFixpoint a1 := cons 0 a1
+with a2 := cons 1 a2.
+(* Why not to allow this definition ?
+CoFixpoint b1 := cons 0 b2
+with b2 := b1.
+*)
+
+End Recursivity.
diff --git a/test-suite/output/bug_12159.out b/test-suite/output/bug_12159.out
new file mode 100644
index 0000000000..7f47c47e32
--- /dev/null
+++ b/test-suite/output/bug_12159.out
@@ -0,0 +1,28 @@
+f 1%B
+ : unit
+f 0
+ : unit
+1%B
+ : unit
+0
+ : unit
+1%B
+ : unit
+1
+ : unit
+1
+ : unit
+0
+ : unit
+1
+ : unit
+0%A
+ : unit
+1
+ : unit
+0%A
+ : unit
+0
+ : unit
+0
+ : unit
diff --git a/test-suite/output/bug_12159.v b/test-suite/output/bug_12159.v
new file mode 100644
index 0000000000..91d66f7f4c
--- /dev/null
+++ b/test-suite/output/bug_12159.v
@@ -0,0 +1,39 @@
+Declare Scope A.
+Declare Scope B.
+Delimit Scope A with A.
+Delimit Scope B with B.
+Definition to_unit (v : Decimal.uint) : option unit
+ := match Nat.of_uint v with O => Some tt | _ => None end.
+Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0.
+Definition of_unit' (v : unit) : Decimal.uint := Nat.to_uint 1.
+Numeral Notation unit to_unit of_unit : A.
+Numeral Notation unit to_unit of_unit' : B.
+Definition f x : unit := x.
+Check f tt.
+Arguments f x%A.
+Check f tt.
+Check tt.
+Open Scope A.
+Check tt.
+Close Scope A.
+Check tt.
+Open Scope B.
+Check tt.
+Undelimit Scope B.
+Check tt.
+Open Scope A.
+Check tt.
+Close Scope A.
+Check tt.
+Close Scope B.
+Check tt.
+Open Scope B.
+Check tt.
+Notation "1" := true.
+Check tt.
+Open Scope A.
+Check tt.
+Declare Scope C.
+Notation "0" := false : C.
+Open Scope C.
+Check tt. (* gives 0 but should now be 0%A *)
diff --git a/test-suite/ssr/simpl_done.v b/test-suite/ssr/simpl_done.v
new file mode 100644
index 0000000000..f5c766209a
--- /dev/null
+++ b/test-suite/ssr/simpl_done.v
@@ -0,0 +1,28 @@
+Require Import ssreflect.
+
+Inductive lit : Set :=
+| LitP : lit
+| LitL : lit
+.
+
+Inductive val : Set :=
+| Val : lit -> val.
+
+Definition tyref :=
+fun (vl : list val) =>
+match vl with
+| cons (Val LitL) (cons (Val LitP) _) => False
+| _ => False
+end.
+
+(** Check that simplification and resolution are performed in the right order
+ by "//=" when several goals are under focus. *)
+Goal exists vl1 : list val,
+ cons (Val LitL) (cons (Val LitL) nil) = vl1 /\
+ (tyref vl1)
+.
+Proof.
+eexists (cons _ (cons _ _)).
+split =>//=.
+Fail progress simpl.
+Abort.
diff --git a/test-suite/ssr/try_case.v b/test-suite/ssr/try_case.v
new file mode 100644
index 0000000000..114bf2cecf
--- /dev/null
+++ b/test-suite/ssr/try_case.v
@@ -0,0 +1,11 @@
+From Coq Require Import ssreflect.
+
+Axiom T : Type.
+Axiom R : T -> T -> Type.
+
+(** Check that internal exceptions are correctly caught in the monad *)
+Goal forall (a b : T) (Hab : R a b), True.
+Proof.
+intros.
+try (case: Hab).
+Abort.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 02:25:16 +0000