From Stdlib Require Import Ascii List String.
From Ltac2 Require Import Ltac2 Printf.
Open Scope string_scope.
Import ListNotations.

(* Tactic that prints a rocq string without adding quotations marks *)
Ltac2 print_string (s : constr) : unit :=
  let s := Std.eval_vm None s in
  let rec to_list (s : constr) : char list :=
    match! s with
    | EmptyString => []
    | String (Ascii ?a ?b ?c ?d ?e ?f ?g ?h) ?s =>
        let i b n := let n := Int.lsl n 1 in match! b with true => Int.add n 1 | _ => n end in
        Char.of_int (i a (i b (i c (i d (i e (i f (i g (i h 0)))))))) :: to_list s
    end in
  let l := to_list s in
  let buf := String.make (List.length l) (Char.of_int 0) in
  List.iteri (String.set buf) l;
  printf "%s" buf.

Definition src := ("From Stdlib Require Import Ascii List String.
From Ltac2 Require Import Ltac2 Printf.
Open Scope string_scope.
Import ListNotations.

(* Tactic that prints a rocq string without adding quotations marks *)
Ltac2 print_string (s : constr) : unit :=
  let s := Std.eval_vm None s in
  let rec to_list (s : constr) : char list :=
    match! s with
    | EmptyString => []
    | String (Ascii ?a ?b ?c ?d ?e ?f ?g ?h) ?s =>
        let i b n := let n := Int.lsl n 1 in match! b with true => Int.add n 1 | _ => n end in
        Char.of_int (i a (i b (i c (i d (i e (i f (i g (i h 0)))))))) :: to_list s
    end in
  let l := to_list s in
  let buf := String.make (List.length l) (Char.of_int 0) in
  List.iteri (String.set buf) l;
  printf ""%s"" buf.

Definition src := (", ").

Definition quote (s : string) : string  :=
  """""""" ++ string_of_list_ascii
    (flat_map (fun c => if (c =? """""""")%char then [c; c] else [c])
       (list_ascii_of_string s)) ++ """""""".

Definition pre := fst src.
Definition post := snd src.
Definition quine := concat """" [pre; quote pre; "", ""; quote post; post].

Lemma trivial : True.
Proof.
  print_string 'quine.
  trivial.
Qed.").

Definition quote (s : string) : string  :=
  """" ++ string_of_list_ascii
    (flat_map (fun c => if (c =? """")%char then [c; c] else [c])
       (list_ascii_of_string s)) ++ """".

Definition pre := fst src.
Definition post := snd src.
Definition quine := concat "" [pre; quote pre; ", "; quote post; post].

Lemma trivial : True.
Proof.
  print_string 'quine.
  trivial.
Qed.