Module Type Expr.


Parameter Sec:Set.

  (*n=card Sec *)
Parameter n:nat.
  
Require Import Ring_cat.
Parameter Zq_ring:RING.
Definition Zq:Type:=Carrier Zq_ring.
Definition OZ:Zq:=Monoid_cat.monoid_unit Zq_ring.
Definition eqZq:=Equal (s:=Zq_ring).
Parameter eqZq_dec:forall a b:Zq,{eqZq a b}+{~(eqZq a b)}.

 (* card Zq=q *)
Parameter q : nat.

Require Import Reals.
Parameter lt_0_q : (0 < INR q)%R.

Parameter Expr:Set->Type.

Parameter min_Expr:(Expr Sec)->(Expr Sec)->(Expr Sec).
Parameter add_Expr:(Expr Sec)->(Expr Sec)->(Expr Sec).
Parameter mult_Expr:(Expr Sec)->(Expr Sec)->(Expr Sec).


End Expr.


Module Type Op_Expr.
Declare Module E:Expr.
Import E.


Require Import Reals.
Require Import listT.

Parameter input:listT (Expr Sec).

(* for (g1,g2,g3,g4):listT (Expr Sec) and (a1,a2,a3,a4):listT Zq
computes  g1^a1.g2^a2.g3^a3.g4^a4 *)
Parameter mex:(listT (Expr Sec))->(listT Zq)->(Expr Sec).



(* normally Sec:=Finset n 
  for eval_poly we take an elt x:=(x1,. ,xn) of type list Zq instead of Sec->Zq
  so to simplify we use a function Fins2list that return an elt of type Sec->Zq like a list of Zq*)
Variable Fins2list : (Sec ->  Zq) ->  listT Zq.


Require Import POLY_ax.
Require Import Pol_is_ring.
Parameter Call:CALL Zq.

Parameter transl : Expr Sec -> Poly n Call.
(*
Fixpoint transl [ e : (Expr Sec) ] : poly :=
 Cases e of
   (secret e') => (consT (!pairT (Zq_cring q) Mon (POS xH) (mon1e e')) (nilT ?))
  | (const e1) => (consT (!pairT (Zq_cring q) Mon e1 mon0) (nilT ?))
  | (mult e1 e2) => (mult_pol_pol (transl e1) (transl e2))
  | (add e1 e2) => (add_pol (transl e1) (transl e2))
 end.
*)

	
End Op_Expr.