(Joint Center)Library quote

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.

Set Implicit Arguments.

Structure tProp := TProp {tProp_statement :> Prop; _ : tProp_statement}.
Lemma claim : tP : tProp, tP.
Hint Resolve claim.

Canonical Structure True_tProp := TProp Logic.I.
Canonical Structure eq_tProp T (x : T) := TProp (erefl x).
Canonical Structure true_tProp := @TProp true (erefl _).
Canonical Structure and_tProp (P Q : tProp) :=
  TProp (conj (claim P) (claim Q)).

Structure postProp (P : Prop) := PostProp {postProp_statement :> tProp; _ : P}.
Canonical Structure tProp_postProp P claimP pP :=
  PostProp (@TProp P claimP) (claim pP).

Delimit Scope n_ary_op_scope with QOP.
Delimit Scope quote_scope with QT.

Fixpoint n_ary n T := if n is n'.+1 then Tn_ary n' T else T.
Notation "n .-ary" := (n_ary n) (at level 2, format "n .-ary") : type_scope.

Module Quotation.

CoInductive n_ary_op T := NaryOp n of n.-ary T.
Notation "f / n" := (@NaryOp _ n f) : n_ary_op_scope.
Definition bind_op T R (op : n_ary_op T) ifun : R :=
  let: NaryOp n f := op in ifun n f.
Definition arity T op := @bind_op T nat op (fun n _n).

Structure type := Pack {sort :> Type; sym; _ : symn_ary_op sort}.
Notation QuoteType sf := (Pack sf%QOP).
Definition symop T := let: Pack _ _ ops := T return sym Tn_ary_op T in ops.

Inductive term S := Var of nat | App of S & seq (term S).

Lemma term_ind' : S (P : term SType),
  ( i, P (Var S i)) →
  ( s a, foldr prod True (map P a) → P (App s a)) →
  ( t, P t).

Notation "''K_' i" := (Var _ i)
  (at level 8, i at level 2, format "''K_' i") : quote_scope.
Notation "''[' s x1 .. xn ]" := (App s (x1%QT :: .. [:: xn%QT] ..))
  (at level 0, s at level 2, x1, xn at level 8,
   format "''[' '[hv' s x1 .. xn ']' ]") : quote_scope.
Notation "''[' s ]" := (App s [::])
  (at level 0, s at level 2, format "''[' s ]") : quote_scope.

Section OneType.

Variable T : type.
Implicit Type P : Prop.
Implicit Type tP : tProp.

Definition Env := @id (seq T).

Fixpoint lookup i e : option T :=
  if i is i'.+1 then lookup i' (behead e) else ohead e.

Definition interp_app (iarg : term (sym T) → option T) :=
  fix loop a n {struct a} : n.-ary Toption T :=
  if n is n'.+1 return n.-ary Toption T
  then fun fif a is t :: a' then obind (loop a' n' \o f) (iarg t) else None
  else fun xif a is [::] then Some x else None.

Fixpoint interp e t := match t with
 | Var ilookup i e
 | App s abind_op (symop s) (interp_app (interp e) a)
 end.

Fixpoint wf (t : term (sym T)) :=
  match t with
  | App s alet: NaryOp n _ := symop s in (n == size a) && all wf a
  | Var _true
  end.

Fixpoint eval x0 e t :=
  match t with
  | Var inth x0 e i
  | App s a
    odflt x0 (bind_op (symop s) (interp_app (fun xSome (eval x0 e x)) a))
  end.

Lemma interp_wf_eval : y0 e t y,
  interp e t = Some ywf teval y0 e t = y.

Definition var_val := @id T.
Definition op_val := var_val.

Structure form e t P := Form {fval; _ : Pinterp e t = Some fval}.
Lemma formP : e t tP f, interp e t = Some (@fval e t tP f).

Structure store i x P := Store {stval; _ : Plookup i stval = Some x}.
Canonical Structure head_store x e :=
  @Store 0 x True (Env (x :: Env e)) (fun _erefl _).
Lemma tail_store_subproof : i x y e tP s,
  e = @stval i x tP slookup i.+1 (y :: e) = Some x.
Canonical Structure tail_store i x y e tP s :=
  Store (@tail_store_subproof i x y e tP s).

Lemma var_form_subproof : i x P (s : store i x P),
  Pinterp (stval s) 'K_i = Some (var_val x).
Canonical Structure var_form i x P s := Form (@var_form_subproof i x P s).

Lemma op_form_subproof : e t tP (f : form e t tP) x,
  x = @fval e t tP finterp e t = Some (op_val x).

Canonical Structure op_form e t tP f x :=
  Form (@op_form_subproof e t tP f x).

Section OpForm.

Variables (s : sym T) (e : seq T).

Fixpoint OpForm_type a xa fa n :=
  if n is n'.+1 then
     x t tP f, OpForm_type (t :: a) (x :: xa) (@fval e t tP f :: fa) n'
  else form e (App s (rev a)) (map op_val (rev xa) = rev fa).

Definition OpForm_rechyp a (xa fa : seq T) n (x : n.-ary T) :=
   a', map op_val (rev xa) = rev fa
  interp e (App s (catrev a' a)) = interp_app (interp e) a' x.

Definition OpForm_rectype a xa fa n (x : n.-ary T) :=
  OpForm_rechyp a xa fa xOpForm_type a xa fa n.

Definition OpForm_basetype P x a :=
  (Pinterp e (App s a) = Some x) → form e (App s a) P.

Lemma OpForm_recproof : a xa fa n (x1 : n.+1.-ary T),
   x t tP f, OpForm_rechyp a xa fa x1
  OpForm_rechyp (t :: a) (x :: xa) (@fval e t tP f :: fa) (x1 x).

Fixpoint OpForm_rec a xa fa n : x, @OpForm_rectype a xa fa n x :=
  if n is _.+1 return x, @OpForm_rectype a xa fa n x then
  fun _ IHx _ _ _ _OpForm_rec (OpForm_recproof IHx) else
  fun x IHx
    (if rev a is (t :: a') as rev_a return OpForm_basetype _ _ rev_a then
     fun IHxForm IHx else fun IHxForm IHx) (IHx [::]).

Lemma OpForm_subproof : bind_op (symop s) (OpForm_rechyp [::] [::] [::]).

Definition OpForm :=
  (let: (op/n)%QOP as op_n := symop s
   return (bind_op op_n _ : Prop) → @OpForm_type _ _ _ (arity op_n) in
   @OpForm_rec _ _ _ n op)
   OpForm_subproof.

End OpForm.

Section GenSimp.

Variable simp : seq Tterm (sym T) → option T.

Definition simp_axiom := e t x y,
  interp e t = Some xsimp e t = Some yx = y.

Hypothesis simpP : simp_axiom.

Structure closed := Closed {closed_val :> seq T}.
Canonical Structure head_closed := Closed (Env [::]).
Canonical Structure tail_closed x (ce : closed) := Closed (x :: ce).
Inductive close : seq TProp := Close (ce : closed) : close ce.
Canonical Structure close_tProp ce := TProp (Close ce).

Lemma simp_form : e t y ptP,
   f : form (Env e) t
      (@postProp_statement (close (Env e) ∧ simp e t = Some y) ptP),
  fval f = y.

End GenSimp.

Definition Econs := Cons.
Definition Etag of nat := @idfun.
Definition Enil := Nil.

Fixpoint simp_env {T'} e i :=
  if e is x :: e' then omap (Econs (Etag i x)) (simp_env e' i.+1)
  else Some (Enil T').

Notation "' 'K_' i := x" := (Etag i x)
  (at level 200, format "' 'K_' i := x") : quote_tag_scope.

Notation "[ 'env' d1 ; .. ; d_n ]" := (Econs d1 .. (Econs d_n (Enil _)) ..)
  (at level 0, format "[ 'env' '[' d1 ; '/' .. ; '/' d_n ] ']'")
   : quote_scope.

Notation "[ 'env' ]" := (Enil _)
  (at level 0, format "[ 'env' ]") : quote_scope.

Lemma unquote_default : falseT.
Definition unquote e t :=
  if interp e t is Some x as ox return oxT then fun _x else
  unquote_default.


Lemma end_unquote : true.
Definition simp_quote e t :=
  obind (fun e'
   (if interp e' t as b return (b_) → _ then
      fun wf_t'Some (unquote (wf_t' end_unquote))
   else fun _None) id)
  (simp_env e 0).

Lemma simp_quoteP : simp_axiom simp_quote.

Definition quote := simp_form simp_quoteP.

End OneType.

End Quotation.

Canonical Structure Quotation.head_store.
Canonical Structure Quotation.tail_store.
Canonical Structure Quotation.var_form.
Canonical Structure Quotation.op_form.
Canonical Structure Quotation.head_closed.
Canonical Structure Quotation.tail_closed.
Canonical Structure Quotation.close_tProp.

Notation QuoteType sf := (Quotation.Pack sf%QOP).
Notation "f / n" := (@Quotation.NaryOp _ n f) : n_ary_op_scope.

Notation OpForm := Quotation.OpForm.

Notation "''K_' i" := (Quotation.Var _ i)
  (at level 8, i at level 2, format "''K_' i") : quote_scope.
Notation "''[' s x1 .. xn ]" :=
  (Quotation.App s (x1%QT :: .. [:: xn%QT] ..))
  (at level 0, s at level 2, x1, xn at level 8,
   format "''[' s '[hv' x1 '/' .. '/' xn ']' ]") : quote_scope.
Notation "''[' s ]" := (Quotation.App s [::])
  (at level 0, s at level 2, format "''[' s ]") : quote_scope.
Notation "' 'K_' i := x" := (Quotation.Etag i x)
  (at level 200, format "' 'K_' i := x") : quote_tag_scope.
Notation "[ 'env' d1 ; .. ; d_n ]" :=
  (Quotation.Econs d1 .. (Quotation.Econs d_n (Quotation.Enil _)) ..)
  (at level 0, format "[ 'env' '[' d1 ; '/' .. ; '/' d_n ] ']'")
   : quote_scope.
Notation "[ 'env' ]" := (Quotation.Enil _)
  (at level 0, format "[ 'env' ]") : quote_scope.

Notation unquote e t := (@Quotation.unquote _ e t%QT _).

CoInductive bool_sym := bTrue | bAnd.
Canonical Structure bool_quoteType :=
  QuoteType (fun smatch s with bTruetrue/0 | bAndandb/2 end).
Canonical Structure and_form := Eval hnf in OpForm bAnd.
Canonical Structure true_form := Eval hnf in OpForm bTrue.

Lemma try_bquote : b1 b2 b3,
  false && b1 && (b2 && true && b3) && (b2 && b1 && b2) = false && b2.

Fixpoint bstore s bt := match bt with
| 'K_iset_nth false s i true
| '[bAnd t1 t2] ⇒ bstore (bstore s t1) t2
| _s
end%QT.

Fixpoint bread ot i s := match s with
| [::] ⇒ odflt '[bTrue] ot
| true :: s'bread (Some (oapp (fun t ⇒ '[bAnd t 'K_i]) 'K_i ot)) i.+1 s'
| false :: s'bread ot i.+1 s'
end%QT.

Fixpoint bnormed t i := match t with
| '[bAnd t' 'K_j] ⇒ bnormed t' 1
| 'K_ji > 0
| '[bTrue] ⇒ i == 0
| _false
end%QT.

Definition bsimp_fn e t :=
  if bnormed t 0 then None else
  Quotation.interp e (bread None 0 (bstore [::] t)).

Lemma bsimpP : Quotation.simp_axiom bsimp_fn.

Definition bsimp := Quotation.simp_form bsimpP.

Lemma try_bsimp : b1 b2 b3,
  true && b1 && (b2 && b3) && (b2 && b1 && b2) = b1 && b2 && true && b3.
Print try_bsimp.