(*
 * A loose reimplementation of the `Logic Programming` chapter of cpdt using coq-elpi.
 *)

From elpi Require Import elpi.

(* Addition as an inductive Property: *)
Inductive plusR : nat -> nat -> nat -> Prop :=
| PlusO : forall m, plusR O m m
| PlusS : forall n m r,
    plusR n m r
    -> plusR (S n) m (S r).

(* Notice how this mirrors the definition in {λ-,}Prolog: *)
Elpi Program plus "
kind nat type.
type zero nat.
type succ nat -> nat.

pred plus o:nat o:nat o:nat.
plus zero M M.
plus (succ N) M (succ R) :-
  plus N M R.
".
Elpi Typecheck.


Elpi Tactic add.
Elpi Accumulate "
pred add_p o:term o:term o:term o:term.
add_p {{O}} N N {{PlusO lp:N}}.
add_p {{S lp:N}} M {{S lp:P}} {{PlusS lp:N lp:M lp:P lp:SubProof}} :-
  add_p N M P SubProof.

solve (goal _Ctx _ {{plusR lp:N lp:M lp:P}} _ _ as G) GS :-
  add_p N M P Proof,
  refine Proof G GS.
solve _ _ :-
  coq.ltac.fail _ ""not an addition"".
".
Elpi Typecheck.

Goal exists x, plusR 4 x 7.
  eexists.
  elpi add.
Qed.

Goal exists x y, plusR x y 4.
  repeat eexists.
  elpi add.
Qed.

Require Import List.
Import ListNotations.

Section lengthR.
Variable A : Set.
Inductive lengthR : list A -> nat -> Prop :=
| lengthNil : lengthR nil O
| lengthCons : forall X Xs N,
    lengthR Xs N ->
    lengthR (cons X Xs) (S N).
End lengthR.

Print lengthR.
Elpi Tactic length.
Elpi Accumulate "
pred length i:term o:term o:term o:term.
length A {{nil}} {{O}} {{lengthNil lp:A}}.
length A {{cons lp:X lp:Xs}} {{S lp:N}} {{lengthCons lp:A lp:X lp:Xs lp:N lp:P}} :-
  length A Xs N P.

solve (goal _Ctx _ {{lengthR lp:A lp:L lp:N}} _ _ as G) GS :-
  length A L N P,
  refine P G GS.

solve _ _ :-
  coq.ltac.fail _ ""could not unify"".
".
Elpi Typecheck.

Elpi Query lp:{{
      length {{nat}} L {{3}} P
}}.

Goal exists l, lengthR nat l 4.
  eexists.
  elpi length.
  Unshelve.
  all: constructor.
Qed.

Elpi Tactic length_choose.
Elpi Accumulate "
pred choose i:term o:term.
choose {{nat}} {{O}}.
choose {{nat}} {{S lp:N}} :-
  choose {{nat}} N.
choose _T _ :-
  coq.ltac.fail _ ""Unsupported type "".

pred length-choose i:term o:term o:term o:term.
length-choose A {{nil}} {{O}} {{lengthNil lp:A}}.
length-choose A {{cons lp:X lp:Xs}} {{S lp:N}} {{lengthCons lp:A lp:X lp:Xs lp:N lp:P}} :-
  choose A X,
  length-choose A Xs N P.

solve (goal _Ctx _ {{lengthR lp:A lp:L lp:N}} _ _ as G) GS :-
  length-choose A L N P,
  refine P G GS.

solve _ _ :-
  coq.ltac.fail _ ""could not unify"".
".
Elpi Typecheck.

Goal exists l, lengthR nat l 4.
  eexists.
  elpi length_choose.
Qed.

Section appendR.
  Variable A : Set.
  Inductive appendR : list A -> list A -> list A -> Prop :=
  | appendNil : forall L,
        appendR nil L L
  | appendCons : forall X Xs Ys Zs,
      appendR Xs Ys Zs ->
      appendR (cons X Xs) Ys (cons X Zs).
End appendR.

Elpi Tactic append.
Elpi Accumulate "
pred append i:term o:term o:term o:term o:term.
append A {{nil}} L L {{appendNil lp:A lp:L}}.
append A {{cons lp:X lp:Xs}} Ys {{cons lp:X lp:Zs}} {{appendCons lp:A lp:X lp:Xs lp:Ys lp:Zs lp:P}} :-
       append A Xs Ys Zs P.

solve (goal _Ctx _ {{appendR lp:A lp:Xs lp:Ys lp:Zs}} _ _ as G) GS :-
  append A Xs Ys Zs P,
  refine P G GS.

solve _ _ :-
  coq.ltac.fail _ ""could not unify"".
".
Elpi Typecheck.

Goal forall L, appendR nat nil L L.
  intros.
  elpi append.
Qed.

Goal exists L, appendR nat [1 ; 2] L [1 ; 2 ; 3 ; 4].
  eexists.
  elpi append.
Qed.

Goal exists L X, appendR nat L [X] ([1 ; 2 ; 3 ]) /\ X = 3.
  eexists.
  eexists.
  split.
  - elpi append.
  - reflexivity.
Qed.

Elpi Tactic length_append.
Elpi Accumulate "
pred append i:term o:term o:term o:term o:term.
append A {{nil}} L L {{appendNil lp:A lp:L}}.
append A {{cons lp:X lp:Xs}} Ys {{cons lp:X lp:Zs}} {{appendCons lp:A lp:X lp:Xs lp:Ys lp:Zs lp:P}} :-
       append A Xs Ys Zs P.

pred length i:term o:term o:term o:term.
length A {{nil}} {{O}} {{lengthNil lp:A}}.
length A {{cons lp:X lp:Xs}} {{S lp:N}} {{lengthCons lp:A lp:X lp:Xs lp:N lp:P}} :-
  length A Xs N P.

solve (goal _Ctx _ {{appendR lp:A lp:Xs lp:Ys lp:Zs}} _ _ as G) GS :-
  append A Xs Ys Zs P,
  refine P G GS.

solve (goal _Ctx _ {{lengthR lp:A lp:L lp:N}} _ _ as G) GS :-
  length A L N P,
  refine P G GS.

solve _ _ :-
  coq.ltac.fail _ ""could not unify"".
".
Elpi Typecheck.

Inductive exp : Set :=
| Const : nat -> exp
| Var : exp
| Plus : exp -> exp -> exp.

Inductive eval (var : nat) : exp -> nat -> Prop :=
| EvalConst : forall n, eval var (Const n) n
| EvalVar : eval var Var var
| EvalPlus : forall e1 e2 n1 n2, eval var e1 n1
  -> eval var e2 n2
  -> eval var (Plus e1 e2) (n1 + n2).

Elpi Tactic eval.
Elpi Accumulate "
pred eval o:term o:term o:term o:term.
eval V {{Const lp:N}} N {{EvalConst lp:V lp:N}}.
eval V {{Var}} V {{EvalVar lp:V}}.
eval V {{Plus lp:E1 lp:E2}} {{lp:N1 + lp:N2}} {{EvalPlus lp:V lp:E1 lp:E2 lp:N1 lp:N2 lp:P1 lp:P2}} :-
  eval V E1 N1 P1,
  eval V E2 N2 P2.

solve (goal _Ctx _ {{eval lp:V lp:T lp:N}} _ _ as G) GS :-
  eval V T N P,
  refine P G GS.

".
Elpi Typecheck.

Elpi Query lp:{{
  eval V {{(Plus Var (Plus (Const 8) Var))}} {{(lp:V + (8 + lp:V))}} P
}}.

Example eval1 : forall var, eval var (Plus Var (Plus (Const 8) Var)) (var + (8 + var)).
intros.
elpi eval.
Qed.