/* $OpenXM: OpenXM/src/asir-contrib/packages/sample/verify-by-sm1,v 1.2 2000/07/17 02:58:46 takayama Exp $ */
/*
How to use?
(1) Add the following lines  to .asirc
load("/home/nobuki/OpenXM/src/asir-contrib/packages/sample/verify-by-sm1");
/home/nobuki/ may be changed to your directory where you put OpenXM
"check_trace" in gr is overriden by that in verify-by-sm1, so
verify-by-sm1 must be read after gr has been read.
(2)
   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);");

*/

extern NFArray;

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 ");
     sm1(Sm1_proc,"[(cmoLispLike) 0] extension ");
  }
  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]);
}

/* This is a copy of check_trace of gr in the asir standard library */
def check_trace(NF,NFIndex,HL)
{
	if ( !car(HL)[0] ) {
		/* dehomogenization */
		DH = dp_dehomo(NFArray[car(HL)[1]]);
		if ( NF == DH ) {
			realloc_NFArray(NFIndex);
			NFArray[NFIndex] = NF;
			return 0;
		} else
			error("check_trace(dehomo)");
	}

	for ( G = 0, T = HL; T != []; T = cdr(T) ) {
		H = car(T);

		Coeff = H[0];
		Index = H[1];
		Monomial = H[2];
		Denominator = H[3];

		Reducer = NFArray[Index];
		/* G = (Coeff*G+Monomial*Reducer)/Denominator; */
        G = sm1_verify00(Coeff,G,Monomial,Reducer,Denominator);
	}
	if ( NF == G ) {
		realloc_NFArray(NFIndex);
		NFArray[NFIndex] = NF;
		return 0;
	} else
		error("check_trace");
}


end$