lambda_calc_quoteless_idents.v

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Ltac2.Ltac2.


(**** Parsing quote-less identifiers into Gallina Strings ****)

(* Takes a list of powers instead of one power and dividing because
   Ltac2 does not have integer division: https://github.com/coq/coq/issues/13802 *)
Ltac2 rec int_to_bits_rec(powers: int list)(val: int) :=
  match powers with
  | p :: rest =>
    if Int.le p val
    then true :: int_to_bits_rec rest (Int.sub val p)
    else false :: int_to_bits_rec rest val
  | [] => []
  end.

(* [2^(n-1); ..., 2^0] *)
Ltac2 rec powers_of_two(n: int) :=
  if Int.equal n 1 then [1] else
  let r := powers_of_two (Int.sub n 1) in
  match r with
  | h :: t => Int.mul 2 h :: r
  | [] => []
  end.

Ltac2 char_to_bits(c: char) :=
  int_to_bits_rec (powers_of_two 8) (Char.to_int c).

Ltac2 bool_to_coq(b: bool) :=
  if b then constr:(true) else constr:(false).

Ltac2 mkApp(f: constr)(args: constr array) :=
  Constr.Unsafe.make (Constr.Unsafe.App f args).

Ltac2 char_to_ascii(c: char) :=
  mkApp constr:(Ascii.Ascii)
        (Array.of_list (List.rev (List.map bool_to_coq (char_to_bits c)))).

Ltac2 rec string_to_coq_rec(s: string)(i: int)(acc: constr) :=
  if Int.lt i 0 then acc else
    let c := char_to_ascii (String.get s i) in
    string_to_coq_rec s (Int.sub i 1) constr:(String.String $c $acc).

Ltac2 string_to_coq(s: string) :=
  string_to_coq_rec s (Int.sub (String.length s) 1) constr:(String.EmptyString).

Ltac2 ident_to_coq(i: ident) := string_to_coq (Ident.to_string i).

Inductive Ltac2IdentToPass := mkLtac2IdentToPass.

(* Trick from https://pit-claudel.fr/clement/papers/koika-dsls-CoqPL21.pdf *)
Ltac serialize_ident_in_context :=
  ltac2:(match! goal with
         | [ h: Ltac2IdentToPass |- _  ] =>
           let s := ident_to_coq h in exact $s
         end).

Notation ident_to_string a :=
  (match mkLtac2IdentToPass return string with
   | a => ltac:(serialize_ident_in_context)
   end) (only parsing).

Check ident_to_string foo.
(* prints
"foo"%string
     : string
*)


(**** Printing Gallina strings without quotes ****)

Declare Custom Entry pr_char.
Notation "'a'" := "a"%char (in custom pr_char).
Notation "'b'" := "b"%char (in custom pr_char).
Notation "'c'" := "c"%char (in custom pr_char).
Notation "'d'" := "d"%char (in custom pr_char).
Notation "'e'" := "e"%char (in custom pr_char).
Notation "'f'" := "f"%char (in custom pr_char).
Notation "'g'" := "g"%char (in custom pr_char).
Notation "'h'" := "h"%char (in custom pr_char).
Notation "'i'" := "i"%char (in custom pr_char).
Notation "'j'" := "j"%char (in custom pr_char).
Notation "'k'" := "k"%char (in custom pr_char).
Notation "'l'" := "l"%char (in custom pr_char).
Notation "'m'" := "m"%char (in custom pr_char).
Notation "'n'" := "n"%char (in custom pr_char).
Notation "'o'" := "o"%char (in custom pr_char).
Notation "'p'" := "p"%char (in custom pr_char).
Notation "'q'" := "q"%char (in custom pr_char).
Notation "'r'" := "r"%char (in custom pr_char).
Notation "'s'" := "s"%char (in custom pr_char).
Notation "'t'" := "t"%char (in custom pr_char).
Notation "'u'" := "u"%char (in custom pr_char).
Notation "'v'" := "v"%char (in custom pr_char).
Notation "'w'" := "w"%char (in custom pr_char).
Notation "'x'" := "x"%char (in custom pr_char).
Notation "'y'" := "y"%char (in custom pr_char).
Notation "'z'" := "z"%char (in custom pr_char).

Declare Custom Entry pr_string.
Notation "" := EmptyString (in custom pr_string, only printing).
Notation "h t" := (String h t)
 (in custom pr_string at level 0, h custom pr_char, t custom pr_string,
  right associativity, format "h t", only printing).

Notation "'pr_string:(' x )" := x
  (x custom pr_string, only printing, format "'pr_string:(' x )").

Notation test_str := "foo"%string (only parsing).

Check test_str.
(* prints
"foo"%string
     : string
*)

Undelimit Scope string_scope.

Check test_str.
(* prints
pr_string:(foo)
     : string
*)


(**** AST of Untyped Lambda Calculus ****)

Inductive expr :=
| EVar(x: string)
| ELam(x: string)(body: expr)
| EApp(f: expr)(arg: expr).


(**** Custom Entry Notations ****)

Declare Custom Entry pa_ident.

Notation "x" := (ident_to_string x)
  (in custom pa_ident at level 0, x ident, only parsing).
Fail Notation "x" := x
  (in custom pa_ident at level 0, x custom pr_string, only printing).
(* Error: Notation "_" in custom pa_ident is already defined
   in pa_ident at level 0 with arguments ident while it is now required to be
   in pa_ident at level 0 with arguments custom pr_string. *)

(* So we have to make separate entries for parsing and printing identifiers: *)
Declare Custom Entry pr_ident.
Notation "x" := x
  (in custom pr_ident at level 0, x custom pr_string, only printing).

Declare Custom Entry pa_expr.
Notation "x" := (EVar x)
  (in custom pa_expr at level 0, x custom pa_ident, only parsing).
Fail Notation "x" := (EVar x)
  (in custom pa_expr at level 0, x custom pr_ident, only printing).
(* Same error, and this problem propagates through the whole grammar,
   so we have to duplicate every rule in a separate entry for parsing
   and another one for printing *)

Declare Custom Entry pr_expr.
Notation "x" := (EVar x)
  (in custom pr_expr at level 0, x custom pr_ident, only printing).

Notation "'expr:(' x )" := x (x custom pa_expr at level 100, only parsing).
(* Same problem again, but this time within constr, and we can work around
   it by adding an extra space inside the keyword which will get collapsed
   into the empty string when printing: *)
Notation "'exp' 'r:(' x )" := x
   (x custom pr_expr at level 100, only printing, format "exp r:( x )").

Notation "( x )" := x
  (in custom pa_expr at level 0, x custom pa_expr at level 100, only parsing).
Notation "( x )" := x
  (in custom pr_expr at level 0, x custom pr_expr at level 100, only printing).

(* Antiquote (fallback to Gallina).
   Useful for working with partially concrete, partially abstract terms,
   for metaprogramming, and also for debugging the printing of Notations:
   If a subterm is not printable, it get wrapped inside `coq:(...)`, so
   it's easier to know where the problem is. *)
Notation "'coq:(' x )" := x
  (in custom pa_expr at level 0, x constr at level 200, only parsing).
Notation "'coq:(' x )" := x
  (in custom pr_expr at level 0, x constr at level 200,
   format "'coq:(' x )", only printing).

Notation "f x" := (EApp f x)
  (in custom pa_expr at level 10, left associativity, only parsing).
Notation "f x" := (EApp f x)
  (in custom pr_expr at level 10, left associativity,
   format "'[  ' f  x ']'", only printing).


Notation "'fun' x => body" := (ELam x body)
  (in custom pa_expr at level 100, x custom pa_ident,
   body custom pa_expr at level 100, only parsing).
Notation "'fun' x y .. z => body" := (ELam x (ELam y .. (ELam z body) ..))
  (in custom pa_expr at level 100,
   x custom pa_ident, y custom pa_ident, z custom pa_ident,
   body custom pa_expr at level 100, only parsing).
Notation "'fun' x => body" := (ELam x body)
  (in custom pr_expr at level 100, x custom pr_ident,
   body custom pr_expr at level 100,
   format "'[  ' 'fun'  x  =>  '/' body ']'", only printing).
Notation "'fun' x y .. z => body" := (ELam x (ELam y .. (ELam z body) ..))
  (in custom pr_expr at level 100,
   x custom pr_ident, y custom pr_ident, z custom pr_ident,
   body custom pr_expr at level 100,
   format "'[  ' 'fun'  x  y  ..  z  =>  '/' body ']'", only printing).

Notation "'let' x := rhs 'in' body" := (EApp (ELam x body) rhs)
  (in custom pa_expr at level 100, x custom pa_ident, rhs custom pa_expr at level 10,
   body custom pa_expr at level 100, only parsing).
Notation "'let' x := rhs 'in' body" := (EApp (ELam x body) rhs)
  (in custom pr_expr at level 100, x custom pr_ident, right associativity,
   format "'[' 'let'  x  :=  '[' rhs ']'  'in'  '/' body ']'", only printing).


(**** Test ****)

Example ChurchNumerals := expr:(
  let zero := fun f x => x in
  let succ := fun m f x => m f (f x) in
  let plus := fun m n f x => m f (n f x) in
  let one := succ zero in
  let two := succ one in
  plus two two
).

Print ChurchNumerals.
(* prints
ChurchNumerals =
expr:(let zero := fun f x => x in
      let succ := fun m f x => m f (f x) in
      let plus := fun m n f x => m f (n f x) in
      let one := succ zero in let two := succ one in plus two two)
     : expr
*)