playground/coq/ltac2-demo.v

(*
Thanks to Yiyun Liu.
 *)

(*
https://github.com/coq/coq/blob/master/user-contrib/Ltac2/
 *)

From Ltac2 Require Import Ltac2.

(* Int is a primitive datatype in ltac2 *)
Ltac2 Eval 1.
Ltac2 Eval Int.add 1 2.

(* Lambda *)
Ltac2 Eval (fun x => x).
Ltac2 Eval (fun x => Int.add x x).
Ltac2 Eval (fun x => Int.add x x) 5.

(* let binding *)
Ltac2 Eval let f := (fun x => Int.add x x) in f 5.

(* An ltac2 function *)
Ltac2 double_int := (fun x => Int.add x x).
Ltac2 Eval double_int 4.

(* Syntactic sugar for the above *)
Ltac2 double_int2 x := Int.add x x.
Ltac2 Eval double_int2 4.

(* Type annotations also possible *)
Ltac2 double_int3 (x:int) := Int.add x x.

(* Like ltac1, no termination check *)
(*
Ltac2 is_even x := Int.equal (Int.mod x 2).

Ltac2 rec collatz n := 
  if Int.le n 1 then 0
  else  
 *)
(* TODO: Comment lines in emacs *)

(* ALlgebraic datateyp *)
Ltac2 Type rec PNat :=
  [ Z | S (PNat) ].

Ltac2 rec padd (m:PNat) (n:PNat) :=
  match m with
  | Z => n
  | S m' => S (padd m' n)
  end.

(* Looks like a less powerful version of ocaml *)
Ltac2 Type rec 'a Tree :=
  [ Empty | Node ('a, 'a Tree, 'a) ].

(* No deptypes in ltac2 *)
Fail Ltac2 rec treeSize (t: 'a Tree) :=
  match t with
  | Empty => 0
  | Node l v r => Int.add 1 (Int.add (treeSize l) (treeSize r))
  end.

Ltac2 Eval '1. (* Gallina term ! *)
Ltac2 Eval '(1,2). (* Gallina term ! *)

Ltac2 Type ('a, 'b) Pair := { fst: 'a; snd: 'b }.
Ltac2 Eval {fst:=1; snd:=2}.
Ltac2 Eval  {fst:=1; snd:=2}.(fst).

(* We can refer to Gallina top-level defns *)
Definition four := 4.
Ltac2 Eval 'four.

(* ' is like constr: in ltac1 *)

Ltac2 Eval (1,true).

Fail Ltac2 Eval four. (* Fails because not an ltac2 variable *)
Fail Ltac2 Eval fst (1,2). (* TODO *)

Ltac2 Eval Int.le 2 3.

(* Gallina term! *)
Ltac2 rec int_n n :=
  match Int.le n 0 with
  | true => '0
  | false =>
      let n' := int_n (Int.sub n 1) in
      '(1 + $n')  (* The $ is like the ' in lisp *)
  end.
Ltac2 Eval int_n 2.
(* - : constr = constr:(1 + (1 + 0)) *)

(* The constructed Gallina terms won't be evaluated. So no type checking *)
Ltac2 rec int_n2 n :=
  match Int.le n 0 with
  | true => 'true
  | false =>
      let n' := int_n (Int.sub n 1) in
      '(1 + $n')  (* The $ is like the ' in lisp *)
  end.


Ltac2 Eval Constr.equal '(fun x:nat => x) '(fun z:nat => z).
(* - : bool = true *)

(* No type annotations => somethign like evar might show up. ie, holes *)
Ltac2 Eval Constr.equal '(fun x => x) '(fun z:nat => z).
(* - : bool = false *)

Ltac2 Eval Constr.equal '(1 + 1) '2.
(* - : bool = false *)

Ltac2 Eval Constr.equal '(1 + 1) (int_n 1).
(* - : bool = false *)


(* Querying proof state *)
Ltac2 Eval Control.hyps.
Ltac2 Eval Control.hyps ().

Section foo.
  Variable x : nat.
  Ltac2 Eval Control.hyps ().
(*
- : (ident * constr option * constr) list = [(@x, None, constr:(nat))]
*)

  Variable y : nat.
  Ltac2 Eval Control.hyps ().
(*
- : (ident * constr option * constr) list = [(@x, None, constr:(nat));
(@y, None, constr:(nat))]
*)

  Parameter z : nat. (* Not change in hyps! *)
  Ltac2 Eval Control.hyps ().
(*
- : (ident * constr option * constr) list = [(@x, None, constr:(nat));
(@y, None, constr:(nat))]
*)
End foo.


Module modfoo.
  Parameter x : nat.
  Ltac2 Eval Control.hyps ().
  (* - : (ident * constr option * constr) list = [] *)
End modfoo.

Ltac2 Eval Control.enter (fun _ => Control.goal (); ()).
Ltac2 Eval Control.enter.

(*************POST*************)
(* Mutable cells *)
Ltac2 mutable x_mut := 3.
Ltac2 Eval x_mut.
Ltac2 Set x_mut := 2.
Ltac2 Eval x_mut.

Ltac2 x_immut := 3.
Fail Ltac2 Set x_immut := 2.
(* The tactic x_immut is not declared as mutable *)

(* Can access old value of a mutable variable with [as] *)
Ltac2 mutable f x := Int.add x 1.
Ltac2 Eval f 3.  (* 4 *)

Ltac2 Set f as oldf := fun x => Int.add 10 (oldf x).
Ltac2 Eval f 3.  (* 14 *)


(*********** Printing **********)

From Ltac2 Require Import Message.
Fail Message.print (Message.of_string "unqualified calls").
Fail Message.print '(1 + 1).

Fail Ltac2 Eval Int.mod 2 3.
(* Gives a list of hypotheses *)

(* TODO:
 - Is it possible to mix ltac1 and ltac2
 - Where to find ltac2 docs
 - How usable is ltac2 at the moment? Maturity-wise? Earlier something being buggy (auto?) was mentioned. 
 - ast print of gllaina term constructed there's a pirnt function or something in library as string 
   + there is something int to string
   + Gives your more control in some sense. You can get out when you want.

 - semicolon is different in ltac2. got to iterate manually or something
 - auto is buggy in ltac2?
 - Ltac2 have states?
 - https://coq.inria.fr/refman/proof-engine/ltac2.html#coq:tacn.lazy_match!
 - evar is a goal, but all goals aren't evar?? said by Irene Yoon??
   *)