(* Elpi as an embedded meta-programming language for Coq *)
From elpi Require Import elpi.
Elpi Program introspection "".

(* We can query the coq environment from within elpi *)
Elpi Query lp:{{
  coq.locate "nat" GR,
  coq.locate "S" GRS
}}.

Definition x := 2.

Elpi Query lp:{{
  coq.locate "x" GR,
  coq.env.typeof GR Ty,
  GR = const C,
  coq.env.const C (some Body) TyC
}}.

(* We can also reference Coq Terms from elpi directly *)

Elpi Query lp:{{
  X = {{1}},
  N = {{nat}}
}}.

(** HOAS of Gallina Terms *)

(** `app` *)
(* type app list term -> term *)

Elpi Query lp:{{
  X = app [{{S}}, {{O}}]      
}}.

(** `fun` *)
(* type fun name -> term -> (term -> term) -> term *)

Definition foo := fun x => x + 1.

Elpi Query lp:{{
  coq.locate "foo" (const F),
  coq.env.const F (some Body) _
}}.

Elpi Query lp:{{
  fun `foo` T B = fun `bar` T B
}}.

(** `prod` *)
(* type prod name -> term -> (term -> term) -> term *)

Definition P := forall (n : nat), Prop.

Elpi Query lp:{{
  coq.locate "P" (const P),
  coq.env.const P (some Body) _    
}}.