(* AUTEURS / AUTHORS :                          *)
(* Judicaël Courant,   Jean-François Monin      *)
(* VERIMAG, Université Joseph Fourier, Grenoble *)
(*                                         2006 *)

(* $Id: LasagnaTerms.v,v 1.10 2006/07/16 23:58:16 monin Exp $ *)

Require Import Terms.

Set Implicit Arguments.

Require Import Bool. (* we want Is_true *)

(* ---------------------------------------------------------------------- *)

Section sec_x.
Variable A : Set.
(* 
 Type \Tx is (xor_term false).
 *)
Inductive xor_term : bool -> Set :=
  | X_Zero : forall b, xor_term b
  | X_ns : forall b, Is_true b -> A -> xor_term b
  | X_Xor : forall b, xor_term true -> xor_term true -> xor_term b
.

(* X_nst denotes the constructor \Ix *)
Definition X_nst := X_ns true I.

(* Useful induction principles *)
Definition Is_true2true b :  (Is_true b) -> xor_term b -> xor_term true :=
  if b return (Is_true b -> xor_term b -> xor_term true)
  then fun _ x => x
  else fun F  => match F with end.

Theorem xor_term_true_ind :
       forall (P : xor_term true -> Prop),
       P (X_Zero true) ->
       (forall a, P (X_ns true I a)) ->
       (forall x y, P x -> P y -> P (X_Xor true x y)) ->
       forall (x : xor_term true), P x.
intros P H_Z H_ns H_Xor. fix 1. intro x. 
assert (H_cut : forall b (t:Is_true b) (x : xor_term b), P (Is_true2true t x));
   [clear x | exact (H_cut true I x)].
(* magic script ; but it hides interesting things
destruct x; destruct b; case t; simpl.
  exact H_Z. 
  case i; clear i; simpl. apply H_ns. 
  apply H_Xor; auto.
*)
intros b t x. generalize t; clear t. case x; clear x b.
  intros b; case b; clear b; intro t; case t; simpl; exact H_Z. 
  intros b; case b; clear b; intros i a t; case t; case i; simpl; apply H_ns. 
  intros b x y; case b; clear b; intro t; case t; simpl. 
   apply H_Xor; apply xor_term_true_ind. 
Qed.

Definition NIs_true2false b :  ~(Is_true b) -> xor_term b -> xor_term false :=
  if b return (~ Is_true b -> xor_term b -> xor_term false)
  then fun f  => match f I with end
  else fun _ x => x.


Theorem xor_term_false_ind :
       forall (P : xor_term false -> Prop),
       P (X_Zero false) ->
       (forall x y, P (X_Xor false x y)) ->
       forall (x : xor_term false), P x.
intros P H_Z H_Xor. intro x. 
assert (H_cut : forall b (f:~Is_true b) (x : xor_term b), P (NIs_true2false f x));
   [clear x | exact (H_cut  false (fun F => F) x)].
intros b f x. generalize f; clear f. case x; clear x b.
  intros b; case b; clear b; simpl; intro f. 
     case (f I).
     exact H_Z. 
  intros b; case b; clear b; simpl; intros i a f.
     case (f I).
     case i.
  intros b x y. case b; clear b; simpl; intro f.
     case (f I). 
     apply H_Xor (*; apply xor_term_true_ind*). 
Qed.

End sec_x.

Implicit Arguments X_Zero [A].

(* ---------------------------------------------------------------------- *)

Section sec_nx.
Variable A : Set.
Inductive nx_term : bool -> Set :=
  | NX_PC : forall b, public_const -> nx_term b
  | NX_SC : forall b, secret_const -> nx_term b
  | NX_sum : forall b, Is_true b -> A -> nx_term b
  | NX_E : forall b, nx_term true -> nx_term true -> nx_term b
  | NX_Hash : forall b, nx_term true -> nx_term true -> nx_term b
.
Definition NX_sumt := NX_sum true I.

Definition nx_forget_isfalse b1 (t: nx_term b1) :
                                ~(Is_true b1) -> forall b, nx_term b :=
   match t in (nx_term b1) return (~ Is_true b1 -> forall b, nx_term b) with
   | NX_PC b1 p => fun _ b => NX_PC b p
   | NX_SC b1 s => fun _ b => NX_SC b s
   | NX_sum b1 tb1 _ =>
       fun ntb1 b => match ntb1 tb1 return (nx_term b) with end
   | NX_E b1 n1 n2 => fun _ b => NX_E b n1 n2
   | NX_Hash b1 n1 n2 => fun _ b => NX_Hash b n1 n2
   end.

Definition nx_forget_false (t : nx_term false) : forall b, nx_term b :=
  nx_forget_isfalse t (fun F => F).

End sec_nx.

Implicit Arguments NX_PC [A].
Implicit Arguments NX_SC [A].

(* ---------------------------------------------------------------------- *)

Require Import Empty.
Require Import Nat2.

Fixpoint lasagna_x (e:alte) : Set :=
  match e with
  | AZ => empty
  | ES o => xor_term (lasagna_n o) false
  end
with lasagna_n (o:alto) : Set :=
  match o with
  | OS e => nx_term (lasagna_x e) false
  end.

(* Lasagna candidate. Warning: eta-inside *)
Definition lasagna_cand_x o := xor_term (lasagna_n o).
Definition lasagna_cand_n e := nx_term (lasagna_x e).

(* ---------------------------------------------------------------------- *)

Unset Implicit Arguments.

Section sec_maps.
Variable A B : Set.

Fixpoint map_xor (f:A->B) b (x:xor_term A b) {struct x} : xor_term B b :=
  match x in (xor_term _ b) return (xor_term B b) with
  | X_Zero b => X_Zero b
  | X_ns b it n => X_ns b it (f n)
  | X_Xor b x1 x2 => X_Xor b (map_xor f true x1) (map_xor f true x2)
  end.


Fixpoint map_nx (f:A->B) b (n:nx_term A b) {struct n} : nx_term B b :=
  match n in (nx_term _ b) return (nx_term B b) with
  | NX_PC b p => NX_PC b p
  | NX_SC b s => NX_SC b s
  | NX_sum b it x => NX_sum b it (f x)
  | NX_E b n1 n2 => NX_E b (map_nx f true n1) (map_nx f true n2)
  | NX_Hash b n1 n2 => NX_Hash b (map_nx f true n1) (map_nx f true n2)
  end.


(* Sometimes a layer should be ignored *)
Inductive mayskip_nx (b: bool) : Set :=
  | MS_no : B -> mayskip_nx b
  | MS_yes : nx_term B b -> mayskip_nx b.

Fixpoint map_nx_sticky 
  (f:A-> forall b, mayskip_nx b) b (n:nx_term A b) {struct n} : nx_term B b :=
  match n in (nx_term _ b) return (nx_term B b) with
  | NX_PC b p => NX_PC b p
  | NX_SC b s => NX_SC b s
  | NX_sum b it x => 
      match f x b with 
      | MS_no y => NX_sum b it y
      | MS_yes t => t
      end
  | NX_E b n1 n2 => NX_E b (map_nx_sticky f true n1) (map_nx_sticky f true n2)
  | NX_Hash b n1 n2 => NX_Hash b (map_nx_sticky f true n1) (map_nx_sticky f true n2)
  end.


Fixpoint map_xor_term (f:A->term) b (x:xor_term A b) {struct x} : term :=
  match x with
  | X_Zero b => Zero
  | X_ns b it n => f n
  | X_Xor b x1 x2 => Xor (map_xor_term f true x1) (map_xor_term f true x2)
  end.

Fixpoint map_nx_term (f:A->term) b (n:nx_term A b) {struct n} : term :=
  match n with
  | NX_PC b p => PC p
  | NX_SC b s => SC s
  | NX_sum b it x => f x
  | NX_E b n1 n2 => E (map_nx_term f true n1) (map_nx_term f true n2)
  | NX_Hash b n1 n2 => Hash (map_nx_term f true n1) (map_nx_term f true n2)
  end.

End sec_maps.

Implicit Arguments map_xor [A B].
Implicit Arguments map_nx [A B].
Implicit Arguments map_nx_sticky [A B].
Implicit Arguments MS_no [B].
Implicit Arguments MS_yes [B b].
Implicit Arguments map_xor_term [A].
Implicit Arguments map_nx_term [A].