/* $OpenXM: OpenXM/src/asir-contrib/packages/sample/verify-by-sm1,v 1.1 2000/07/15 07:17:58 takayama Exp $ */
/*
How to use?
(1) Modify OpenXM_contrib2/asir2000/lib/gr as explained below in sm1_verify00
    and save the modified gr by the name 
    OpenXM/src/asir-contrib/packages/sample/gr-tmp
(2) Add the following lines  to .asirc
load("/home/nobuki/OpenXM/src/asir-contrib/packages/sample/gr-tmp");
load("/home/nobuki/OpenXM/src/asir-contrib/packages/sample/verify-by-sm1");
/home/nobuki/ may be changed to your directory where you put OpenXM
(3)
   Starting asir
     Sid = ox_launch();
     dp_gr_flags(["GenTrace",1,"OXCheck",Sid]);
     ox_cmo_rpc(Sid,"dp_ord",Ord);
     ox_execute_string(Sid,"sm1_init_verify(1);");
     gr([x^2+y^2-1,x*y-1],[x,y],0);

     gr(katsura(5),[u0,u1,u2,u3,u4,u5],0);
RESTRICTIONS:
     Only graded reverse lexicographic order can be used.
     The number of variables must be even.
     The number of variables 2*n should be specified by the command
     ox_execute_string(Sid,"sm1_init_verify(n);");

*/

Sm1_proc = -1$

#define SM1_FIND_PROC(P)  P = getopt(proc);\
                          if (type(P) == -1) {\
                             P = sm1_find_proc();\
                          }

def sm1_find_proc() {
  extern Sm1_proc;
  if (Sm1_proc == -1) {
     A = ox_get_serverinfo();
     /* Look for ox_sm1. Not yet written */
     /* Start sm1 automatically if there is not ox_sm1 */
     Sm1_proc = sm1_start();
     sm1(Sm1_proc,"[(Strict) 0] system_variable ");
  }
  return(Sm1_proc);
}

def sm1_init_verify(N) {
  SM1_FIND_PROC(P);
  sm1(P,"[(Strict) 0] system_variable ");
  ox_push_cmo(P,ntoint32(N));
  sm1(P," /nn set ");
  sm1(P,"[(defaultPolyRing) nn] extension ");
  print("sm1_init_verify: the number of variables must be ",0);
  print(N*2);
}

/* Computation of G 
      G = (Coeff*G-Monomial*Reducer)/Divisor;  
   by sm1 */
/*
    NOTE:
    No rational coefficient is allowed.
    Coeff, Monomial, Reducer must not be zero.
*/
/* 
   Replace
     G = (Coeff*G+Monomial*Reducer)/Denominator; 
   by
    sm1_verify00(Coeff,G,Monomial,Reducer,Denominator);
   in check_trace(NF,NFIndex,HL) in gr
*/
def sm1_verify00(Coeff,G,Monomial,Reducer,Denominator) {
   SM1_FIND_PROC(P);
   ox_push_cmo(P,Coeff);
   if (G != 0) {
     ox_push_cmo(P,G);
   }else{
     sm1(P," (0). ");
   }
   sm1(P," mul ");
   ox_push_cmo(P,Monomial);
   ox_push_cmo(P,Reducer);
   sm1(P," mul add /ff set ");
   sm1(P," ff message ");
   ox_push_cmo(P,Denominator);
   sm1(P," /gg set ");
   sm1(P,"[(divByN) ff gg] gbext 0 get");
   G = ox_pop_cmo(P);
   return(G);
}

def check_example() {
   Coeff = 123;
   G = 10*<<0,0,0,0,0,0,0,0>> ;
   Monomial = 6*<<1,2,3,4,0,1,1,1>>;
   Reducer = 4*<<1,0,0,0,1,1,1,1>>+2*<<1,3,0,5,1,1,1,1>>;
   Denominator = 2;

   G2 = (Coeff*G+Monomial*Reducer)/Denominator; 
   /* Computing G2 by sm1 */
   G = sm1_verify00(Coeff,G,Monomial,Reducer,Denominator);

   return([G,G2]);
}

end$