Quelle ltac2_printf.v Sprache: Coq

Require Import Ltac2.Ltac2.
Require Import Ltac2.Printf.

(* Check that the arguments have type unit *)
Ltac2 ignore (x : unit) := ().

Ltac2 dummy0 (_ : int) := Message.of_string "dummy".
Ltac2 dummy (_ : unit) (_ : int) := Message.of_string "dummy".

(** Simple test for all specifications *)

Ltac2 Eval ignore (printf "%i" 42).
Ltac2 Eval ignore (printf "%s" "abc").
Ltac2 Eval ignore (printf "%I" @Foo).
Ltac2 Eval ignore (printf "%t" '(1 + 1 = 0)).
Ltac2 Eval ignore (printf "%%").
Ltac2 Eval ignore (printf "%a" dummy 18).
Ltac2 Eval ignore (printf "%A" dummy0 18).
Ltac2 Eval ignore (printf "%m!" (fprintf "%s %s" "hello" "world")).

(** More complex tests *)

Ltac2 Eval ignore (printf "%I foo%a bar %s" @ok dummy 18 "yes").
Ltac2 Eval ignore (printf "%I foo%A bar %s" @ok dummy0 18 "yes").

Ltac2 Eval Message.print (fprintf "%I foo%a bar %s" @ok dummy 18 "yes").
Ltac2 Eval Message.print (fprintf "%I foo%A bar %s" @ok dummy0 18 "yes").

(** Failure tests *)

Fail Ltac2 Eval printf "%i" "foo".
Fail Ltac2 Eval printf "%s" 0.
Fail Ltac2 Eval printf "%I" "foo".
Fail Ltac2 Eval printf "%t" "foo".
Fail Ltac2 Eval printf "%a" (fun _ _ => ()).
Fail Ltac2 Eval printf "%A" (fun _ => ()).
Fail Ltac2 Eval printf "%a" (fun _ i => Message.of_int i) "foo".
Fail Ltac2 Eval printf "%A" Message.of_int "foo".
Fail Ltac2 Eval printf "%m" 0.

Import Message.

Ltac2 Eval
  Control.assert_true (
    String.equal
      (Message.to_string Message.empty)
      (Message.to_string (Message.of_string ""))
  ).

Ltac2 print_if b fmt :=
  if b then Format.kfprintf Message.to_string fmt
  else Format.ikfprintf Message.to_string (Message.of_string "") fmt.

Ltac2 Notation "print_if" b(tactic(0)) fmt(format) := print_if b fmt.

Ltac2 Eval Control.assert_true (String.equal "hello friend" (print_if true "hello %s" "friend")).

Ltac2 Eval Control.assert_true (String.equal "" (print_if false "hello %s" "friend")).

Fail Ltac2 Eval print_if true "%a" (fun _ => Control.throw Assertion_failure) ().
Fail Ltac2 Eval print_if true "%A" (fun _ => Control.throw Assertion_failure) ().

(* ikfprintf doesn't run the closure *)
Ltac2 Eval print_if false "%a" (fun _ => Control.throw Assertion_failure) ().
Ltac2 Eval print_if false "%A" (fun _ => Control.throw Assertion_failure) ().

quality100%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.