// The structure of CASLtoPVS is directly based on the mapping of basic CASL specifications 
// onto ATerms presented in http://adam.wins.uva.nl/~markvdb/cofi/aterms-basic.html
// I.e. every 'trans' function refers directly to some part of the mapping and so to some
// construct in CASL.  

import java.util.*;
import java.io.*;
import aterm.*;

public class CASLtoPVS {

    StringBuffer pvsspec; // This stores the pvs specification
    Hashtable datatypes;  
    // a global datastructure, storing measures for each defined datatype
    File output;
    FileWriter out;
    String specName;

    static int axiomNo=0;    // for axiom naming scheme.

    public static void main (String args[]) throws java.io.IOException {
	CASLtoPVS c = new CASLtoPVS(args[0]);
	
    }
    // Constructor - initialises files, calls translate function and outputs to file.
    
    public CASLtoPVS (String specTitle) throws java.io.IOException {
	pvsspec=new StringBuffer ();
	datatypes = new Hashtable();
	File input = new File ("./"+specTitle+".aterm");
	FileInputStream instream = new FileInputStream(input);
	ATerm named_spec = ATerm.readFromTextFile (instream);
	
	
	Vector v = named_spec.match ("LIB-ITEM* ( [spec-defn(<term>,<term>,<term>)])");//gives SPEC-NAME, GENERICITY,SPEC
	
	specName = transID((ATerm)v.elementAt(0));
	
	File outdir = new File ("./"+specName);
	outdir.mkdir();

	output = new File ("./"+specName+"/"+specName+".pvs");

	FileWriter outstream=new FileWriter(output);

        transBASIC_SPEC (named_spec);
	
	System.out.println(pvsspec.toString());
	outstream.write(pvsspec.toString());
	outstream.flush();
	outstream.close();
	
	}
	
    void transBASIC_SPEC (ATerm named_spec) throws java.io.IOException{
	Vector v = named_spec.match ("LIB-ITEM* ( [spec-defn(<term>,<term>,<term>)])");//gives SPEC-NAME, GENERICITY,SPEC
	
	ATerm basic_items = (ATerm)(v.elementAt(2));
	
	pvsspec.append (specName+":THEORY\nBEGIN\n");
	transBASIC_ITEMS(basic_items);
	pvsspec.append ("END "+specName);
    }

    void transBASIC_ITEMS (ATerm basic_items) throws java.io.IOException {

	//produce list of basic items
	ATermList  bi=(ATermList)(basic_items.match 
				  ("BASIC-SPEC(basic-spec(BASIC-ITEMS*(<term>)))")).elementAt (0);
	while (!(bi.isEmpty())) {
	    ATermAppl b =(ATermAppl)bi.getFirst() ;

	    /////////////////
	    //Signature items
	    /////////////////

	    if (b.getName() == "SIG-ITEMS") {
		transSIG_ITEMS(b);
		pvsspec.append("\n");

		/////////////////
		// Free datatypes
		/////////////////

	    }else if (b.getName()== "free-datatype") {
		StringBuffer measure=new StringBuffer("reduce_nat(");//provide measure for dt

		//Dealing with datatypes
		ATermList dtlist=(ATermList) 
		    (b.match("free-datatype(DATATYPE-DECL+(<term>))")).elementAt(0);
		while (! dtlist.isEmpty()) {
		    ATermList paramlist=(ATermList) ATerm.parse("[]");
		    StringBuffer dtype = new StringBuffer("BEGIN\n");
		    ATerm dt=dtlist.getFirst();
		    Vector v=dt.match("datatype-decl(<term>,ALTERNATIVE+(<term>))");
		    String typename=transID((ATerm)v.elementAt(0));

		    //Dealing with alternatives
		    ATermList altlist=(ATermList)v.elementAt(1);
		    int altNo=1;

		    while (! altlist.isEmpty()) {
			ATermAppl alt=(ATermAppl)altlist.getFirst();
			if (alt.getName()=="total-construct") {
			    Vector u=alt.match("total-construct(<term>,COMPONENTS*(<term>))");
			    String consname=transID((ATerm)u.elementAt(0));
			    dtype.append(consname);//constructor name

			    //Dealing with components
			    String selectorType=new String();
			    int selectNo=1;// For generating names for added selectors
			    ATermList complist=(ATermList)u.elementAt(1);
			    
			    //if the constructor has no argument then measure does this
			    if (complist.isEmpty()) {
				measure=measure.append("0");
			    }
			    
			    if (! complist.isEmpty()) {
				dtype=dtype.append("(");
				
				//measure stuff
				StringBuffer mconsarg=new StringBuffer("LAMBDA(");
				StringBuffer mconsterm=new StringBuffer(":");
				int margNo=1;
				
				while(! complist.isEmpty()){
				    
				    ATermAppl comp=(ATermAppl)complist.getFirst();
				    if(comp.getName()=="total-select"|comp.getName()=="partial-select") {
					Vector w = comp.match("partial-select(OP-NAME+(<term>),<term>)");
					if (w==null) {
					    w=comp.match("total-select(OP-NAME+(<term>),<term>)");
					}// Treating total and partial selectors the same.
					
					ATermList selectorList=(ATermList)w.elementAt(0);
					selectorType=transID((ATerm)w.elementAt(1));
					
					while(! selectorList.isEmpty()) {
					    ATerm selector=selectorList.getFirst();
					    dtype=dtype.append(transID(selector));
					    selectorList=selectorList.getNext();
					    
					    //measure stuff
					    mconsarg=mconsarg.append("x"+margNo);
					    if (selectorType.equals(typename)) {
						mconsterm=mconsterm.append("x"+margNo+"+");
					    }
					    
						
					    if (! selectorList.isEmpty()) {
						dtype=dtype.append(",");
						mconsarg=mconsarg.append(",");
					    }
					    margNo++;
					    
					}
					dtype=dtype.append(":"+selectorType);
					
					//To mconsarg add selectorType or nat
					if (selectorType.equals(typename)) {
					    mconsarg.append(":nat");
					} else {
					    mconsarg=mconsarg.append(":"+selectorType);
					}
					
				    } else {
					Vector w=comp.match("SORT(<term>)");
					selectorType = transID((ATerm)w.elementAt(0));
					dtype=dtype.append
					    (typename+"cons"+altNo+"select"+selectNo+":"
					     +selectorType);
					selectNo++;
					
					//measure stuff
					mconsarg=mconsarg.append("x"+margNo+":"+selectorType);
					if (selectorType.equals(typename)) {
					    mconsterm=mconsterm.append("c"+margNo+"+");
					}
					
				    }
				    complist=complist.getNext();
				    if (! complist.isEmpty()) {
					dtype=dtype.append(",");
					mconsarg=mconsarg.append(",");
				    }
				    
				//add this selector type to params list if necessary
				    if (! selectorType.equals(typename)
					& paramlist.indexOf(ATerm.parse(selectorType),0)==-1) {
					
					paramlist=paramlist.append(ATerm.parse(selectorType));
					
				    }
				    }
				dtype=dtype.append(")");
				
				//Putting together Lambda term for the this constructor in measure 
				measure=measure.append(mconsarg+")"+mconsterm+"1");

				
				
			    }
			    
			    //Finished dealing with components
			    
			    dtype=dtype.append(":"+typename+"cons"+altNo+"?\n");
			    altNo++;


			    
			} else if (alt.getName()=="partial-construct") {
			    System.out.println("Error - partial constructor");
			} else if (alt.getName()=="subsorts") {
			    System.out.println("Cannot deal with subsorts alternative");
			} else {
			    System.out.println("error, incorrect alternative - "+alt);//debug
			}
			
			altlist=altlist.getNext();
		     
			if (!altlist.isEmpty()) {
			    measure=measure.append(",");
			}

		    }// Finished dealing with alternatives
		    
		    //Gather everything together.
		    
		    StringBuffer params=new StringBuffer();
		    while (! paramlist.isEmpty()) {
			params=params.append(paramlist.getFirst());
			paramlist=paramlist.getNext();
			if (! paramlist.isEmpty()) {params=params.append(",");}
		    }
		    
		    // IMPORT pvs datatype into main spec
		    pvsspec.append("IMPORTING "+typename+"_adt");
		    if (! (params.toString()).equals("")){
			pvsspec=pvsspec.append("["+params+"]");
		    }
		    pvsspec=pvsspec.append("\n\n");

		    //Create .pvs file for datatype
		    File dtoutput = new File("./"+specName+"/"+typename+".pvs");
		    FileWriter dtoutstream = new FileWriter(dtoutput);
		    dtoutstream.write(typename);
		    if (! (params.toString()).equals("")) {
			dtoutstream.write("["+params+":TYPE]");
		    }
		    dtoutstream.write(": DATATYPE\n"+dtype+"\nEND "+typename);
		    dtoutstream.flush();
		    dtoutstream.close();

		    //Putting measure together
		    measure=measure.append(")");
		    datatypes.put(typename,measure.toString());//inserting into hashtableg
					     

		    dtlist=dtlist.getNext();
		}

		/////////////////
		// Variable items
		/////////////////

	    } else if (b.getName() == "var-items") {
		ATermList var_decls = (ATermList)(b.match("var-items(VAR-DECL+(<term>))")).elementAt(0);
		while (! var_decls.isEmpty()) {
		    
		    transVAR_DECL(var_decls.getFirst(),true);
		    pvsspec.append("\n");
		    var_decls=var_decls.getNext();
		    pvsspec.append("\n");
		}

		////////////////////////
		// Local Variable axioms
		////////////////////////

	    } else if (b.getName() == "local-var-axioms") {
		Vector lva = b.match("local-var-axioms(VAR-DECL+(<term>),FORMULA+(<term>))");
		ATermList FORMULAE =(ATermList)lva.elementAt(1);
		// ATerm list of Formulae
		ATermList var_decls=(ATermList)lva.elementAt(0);
		
		// Local variable axioms are equivalent to universally quantifying all 
		// the variables for each axiom, so this is what happens here.

		while (!(FORMULAE.isEmpty())) {
		    ATerm f=FORMULAE.getFirst();
		    ATerm g=ATerm.make ("quantification (forall,VAR-DECL+(<term>),<term>)",var_decls
					,f);
		    pvsspec.append("Axiom"+axiomNo+": AXIOM ");
		    axiomNo++;
		    transFORMULA (g);
		    pvsspec.append("\n");
		    FORMULAE = FORMULAE.getNext();
		}
		pvsspec.append("\n");

		//////////////////////
		// Axioms and theorems
		//////////////////////

	    } else if (b.getName() == "axiom-items") {
		ATermList FORMULAE=(ATermList)(b.match("axiom-items(FORMULA+(<term>))")).elementAt(0);
		while (!(FORMULAE.isEmpty())) {

		    // Test if a theorem
		    ATerm theorem = FORMULAE.getFirst();
		    Vector f=theorem.match
			("quantification(forall,VAR-DECL+([var-decl(VAR+([SIMPLE-ID(WORDS(\"f\"))]),TOKEN-ID(TOKEN(WORDS(\"THEOREM\"))))]),<term>)");
		    if (! (f==null)) {
			pvsspec.append("Theorem"+axiomNo+": THEOREM ");
			transFORMULA((ATerm)f.elementAt(0));

			// if not a theorem -
		    } else {

			pvsspec=pvsspec.append("Ax"+axiomNo+": AXIOM ");
			transFORMULA (FORMULAE.getFirst());
		    }
		    axiomNo++;
		    pvsspec=pvsspec.append("\n");
		    FORMULAE = FORMULAE.getNext();
		}
		pvsspec.append("\n");

		//////////////////////////////
		// Sort generation constraints
		//////////////////////////////

	    } else if (b.getName() == "sort-gen") {
		// Still to be worked out
	    }
	    else System.out.println("Incorrect BASIC ITEM "+b.getName());//debug
	    bi=bi.getNext();
	}
    }
    
    void transSIG_ITEMS (ATerm sig_items) {
	
	ATermAppl si=(ATermAppl)(sig_items.match("SIG-ITEMS(<appl>)")).elementAt(0);
	
	if (si.getName()=="sort-items") {
	    ATerm sort_item = (ATerm)(si.match ("sort-items(<term>)")).elementAt(0);
	    transSORT_ITEMS(sort_item);

	} else if (si.getName()=="op-items") {
	    ATerm op_items=(ATerm) (si.match("op-items(<term>)")).elementAt(0);
	    transOP_ITEMS(op_items);

	} else if (si.getName()=="pred-items") {
	    ATerm pred_items=(ATerm) (si.match ("pred-items(<term>)")).elementAt(0);
	    transPRED_ITEMS(pred_items);

	    //////////////////////////////////////
	    //'Non-free' datatypes
	    //////////////////////////////////////
	} else if (si.getName()=="datatype-items") {
	    ATermList dtlist = (ATermList) 
		(si.match("datatype-items(DATATYPE-DECL+(<term>))")).elementAt(0);
	    while(! dtlist.isEmpty()) {
		ATerm dt = dtlist.getFirst();
		Vector v=dt.match("datatype-decl(<term>,ALTERNATIVE+(<term>))");
		ATerm typeName=(ATerm) v.elementAt(0);

		//Dealing with alternatives
		pvsspec.append(transID(typeName)+": TYPE+\n");

		ATermList altlist=(ATermList) v.elementAt(1);
		int altno=1;
		ATermList snames=(ATermList)ATerm.parse("[]");
		//To remember selector names for axioms.
		
		while (! altlist.isEmpty()) {
		    ATermAppl a=(ATermAppl)altlist.getFirst();
		    if (a.getName()=="total-construct") {
			Vector u=a.match("total-construct(<term>,COMPONENTS*(<term>))");
			ATerm consname=(ATerm)u.elementAt(0);
			pvsspec=pvsspec.append
			    (transID(typeName)+"cons"+altno+"?: TYPE+ FROM "+transID(typeName)+"\n");
			
			//Dealing with components
			ATermList consargs = (ATermList)ATerm.parse("[]");
			ATermList complist=(ATermList)u.elementAt(1);
			while (! complist.isEmpty()) {
			    ATermAppl comp = (ATermAppl)complist.getFirst(); 
			    if(comp.getName()=="total-select"|comp.getName()=="partial-select") {
				Vector w = comp.match("partial-select (OP-NAME+(<term>),<term>)");
				
				if(w==null) {
				    w=comp.match("total-select(OP-NAME+(<term>),<term>)");
				}//Treating total and partial selectors the same.
				
				ATermList selectorlist=(ATermList)w.elementAt(0);
				ATerm selectorType=(ATerm) w.elementAt(1);
				
				while (! selectorlist.isEmpty()) {
				    ATerm selectorName = selectorlist.getFirst();
				    snames=snames.append(selectorName);
				    pvsspec=pvsspec.append
					(transID(selectorName)+":["+transID(typeName)+
					 "cons"+altno+"?->"+transID(selectorType)+"]\n");
				    consargs=consargs.append(selectorType);
				    selectorlist=selectorlist.getNext();
				}
				
				    
				    complist=complist.getNext();				
				} else {
				    //Sort Component
				    consargs=consargs.append(comp);
				    snames=snames.append(ATerm.parse("null-selector"));
				}
			    
			}//finished dealing with componets
			
			pvsspec.append(transID(consname)+":");
			if (!consargs.isEmpty()) {
			    pvsspec.append("[");
			    for (int i=0;i<consargs.getLength();i++) {
				pvsspec.append(transID(consargs.elementAt(i)));
				if (i<consargs.getLength()-1) {
				    pvsspec.append(",");
				}
			    }
			    pvsspec.append("->");
			}
		    
			pvsspec.append(transID(typeName)+"cons"+altno+"?");
			if (!consargs.isEmpty()) {
			    pvsspec.append("]");
			}
			pvsspec.append("\n");
			
			//Now for appropriate axioms.
			for (int i=0;i<snames.getLength();i++) {
			    ATerm sel=snames.elementAt(i);
			    if (! (((ATermAppl)sel).getName()=="null-selector")) {
				pvsspec.append(transID(typeName)+"_"+transID(sel)+"_"+transID(consname)+
					       ": AXIOM (FORALL (");
				for (int j=0;j<consargs.getLength();j++) {
				    pvsspec.append("x"+(j+1)+":"+transID((ATerm)consargs.elementAt(j)));
				    if (! (j==consargs.getLength()-1)) {
					pvsspec.append(",");
				    }
				}
				pvsspec.append("): "+transID(sel)+"("+transID(consname)+"(");
				for (int k=0;k<consargs.getLength();k++) {
				    pvsspec.append("x"+(k+1));
				    if (! (k==consargs.getLength()-1)) {
					pvsspec.append(",");
				    }
				}
			    
				pvsspec.append("))=x"+(i+1)+")\n");
			    }
			}
			altlist=altlist.getNext();
			    
			altno++;
		    
		    } else if (a.getName()=="partial-construct") {
			System.out.println("error partial constructor!");
		    
		    } else if (a.getName()=="sort") {
			System.out.println("Can't handle sort alternative");
		    }
		    
			
			//Finished dealing with alternatives.
		}
		dtlist=dtlist.getNext();
		
	    }
	    
	} else System.out.println("Incorrect SIG ITEM name "+si.getName());//debug
    }
    
    void transSORT_ITEMS (ATerm sort_items) {
	ATermList si=(ATermList)(sort_items.match ("SORT-ITEM+(<term>)")).elementAt(0);
	
	while (!(si.isEmpty())) {
	    ATermAppl a=(ATermAppl) si.getFirst();

	    // sort declaration
	    if (a.getName()=="sort-decl") {
		ATermList sorts=(ATermList)(a.match("sort-decl(SORT+(<term>))")).elementAt(0);
		pvsspec.append(transID(sorts.getFirst()));
		sorts=sorts.getNext();
		while (! sorts.isEmpty()) {
		    pvsspec.append(","+transID(sorts.getFirst()));
		    sorts=sorts.getNext();
		}
		pvsspec.append(": TYPE+\n");

		//subsort declaration
	    } else if (a.getName()=="subsort-decl") {
		Vector v = (a.match ("subsort-decl(SORT+(<term>),<term>)"));
		ATermList subsorts = (ATermList)v.elementAt(0);
		if (! subsorts.isEmpty()) {
		    pvsspec.append(transID(subsorts.getFirst()));
		    subsorts=subsorts.getNext();
		    while (! subsorts.isEmpty()) {
			pvsspec.append(","+transID(subsorts.getFirst()));
			subsorts=subsorts.getNext();
		    }
		}
		ATerm supersort = (ATerm) v.elementAt(1);
		pvsspec.append(":TYPE+ FROM "+transID(supersort)+"\n");
		
		//subsort definition
	    } else if (a.getName()=="subsort-defn") {
		Vector v = a.match ("subsort-defn(<term>,<term>,<term>,<term>)");
		
		String subsort = transID((ATerm)v.elementAt(0)); //subsort
		pvsspec.append (subsort+":TYPE = {"+transID((ATerm)v.elementAt(1))+":"+
				transID((ATerm) v.elementAt(2))+"|");
		
		ATerm Formula = (ATerm)v.elementAt(3);
		transFORMULA(Formula); 
		pvsspec.append("}\n");

		// isomorphism declaration
	    } else if (a.getName()=="iso-decl") {
		ATermList sortlist = (ATermList) (a.match("iso-decl(SORT+(<term>))")).elementAt(0);
		ATerm firstsort = sortlist.getFirst();
		transSORT_ITEMS(ATerm.make("SORT-ITEM+([sort-decl(SORT+([<term>]))])",firstsort));
		sortlist=sortlist.getNext();
		transSORTS(ATerm.make("sorts(SORT*(<term>))",sortlist));
		pvsspec.append(": TYPE+ = "+transID(firstsort)+"\n");
		
	    } else System.out.println("Incorrect SORT ITEM name "+a.getName());//debug
	    si=si.getNext();  
	}
    }

    void transOP_ITEMS (ATerm op_items) {
	ATermList oi=(ATermList) op_items.match("OP-ITEM+(<term>)").elementAt(0); //list of op-items
	while (!(oi.isEmpty())) {
	    ATermAppl a = (ATermAppl)oi.getFirst();

	    // operation declaration
	    if (a.getName()=="op-decl"){
		Vector v=a.match ("op-decl(OP-NAME+(<term>),<term>,OP-ATTR*(<term>))");

		//OP-NAMES//
		ATermList op_names = (ATermList) v.elementAt(0);
		if (! op_names.isEmpty()) {
		    pvsspec.append(transID(op_names.getFirst()));
		    op_names=op_names.getNext();
		    while (! op_names.isEmpty()) {
			pvsspec.append(","+transID(op_names.getFirst()));
			op_names=op_names.getNext();
		    }
		}
		pvsspec.append(":");
		
		//OP-TYPES//
		ATerm op_type = (ATerm)v.elementAt(1);
		transOP_TYPE(op_type);
		pvsspec.append("\n");

		//OP-ATTRIBUTES//
		ATermList opAtts=(ATermList)v.elementAt(2);
		ATerm sort=(ATerm) op_type.match("total-op-type(<term>,<term>)").elementAt(1);
		String s=transID(sort);
		
		while (! opAtts.isEmpty()) {
		    op_names = (ATermList)v.elementAt(0);
		    ATermAppl b = (ATermAppl)opAtts.getFirst();
		    while (! op_names.isEmpty()) {
			ATerm c=op_names.getFirst();
			String name = transID(c);
			
			if (b.getName()=="associative") {
			    pvsspec.append("Ax"+axiomNo+":AXIOM FORALL (x,y,z:"+s+"): "
					   +name+"(x,"+name+"(y,z))="+name+"("+name+"(x,y),z)\n");
			    axiomNo++;
			} else if (b.getName()=="commutative") {
			    pvsspec.append("Ax"+axiomNo+":AXIOM FORALL (x,y:"+s+"): "+name
					   +"(x,y)="+name+"(y,x)\n");
			    axiomNo++;
			} else if (b.getName()=="idempotent") {
			    pvsspec.append("Ax"+axiomNo+": AXIOM FORALL (x:"+s+"): "
					   +name+"(x,x)=x\n");
			    axiomNo++;
			} else if (b.getName()=="unit-op-attr") {
			    ATerm term=(ATerm)b.match("unit-op-attr(<term>)").elementAt(0);
			    pvsspec.append("Ax"+axiomNo+": AXIOM FORALL (x:"+s+"): "+name
					   +"(");
			    transTERM (term);
			    pvsspec.append(",x)=x AND "+name+"(x,");
			    transTERM (term);
			    pvsspec.append (")=x\n");
			    axiomNo++;
			} else System.out.println("Incorrect Attribute name "+b.getName());//debug
			op_names=op_names.getNext();
		    }
		    opAtts=opAtts.getNext();
		}
	    }

	    // operation definition
	    else if (a.getName()=="op-defn") {

		// rec indicates whether the 'RECURSIVE' keyword should be used
		// in the OP-HEAD
		boolean rec=false;
		Vector v=a.match ("op-defn(<term>,<term>,<term>)");
		String name = transID((ATerm) v.elementAt(0));
		StringBuffer measure = new StringBuffer();
		pvsspec.append(name+" ");
		if (isRecursive((ATerm)v.elementAt(0),(ATerm)v.elementAt(2))) {
		    measure = measure.append("MEASURE "+
					     getMeasure((ATerm)v.elementAt(1))+"\n");
		    rec=true;
		}
		
		transOP_HEAD((ATerm)v.elementAt(1),rec);
		pvsspec.append("=");
		transTERM((ATerm)v.elementAt(2));
		pvsspec.append("\n"+measure);
	    }
	    oi=oi.getNext();
	}
    }
    
    void transOP_TYPE (ATerm op_type) {
	if(((ATermAppl)op_type).getName()=="total-op-type") {
	    Vector v=op_type.match("total-op-type(sorts(SORT*(<term>)),<term>)");
	    ATermList argSorts=(ATermList)v.elementAt(0);
	    String resultSort=transID((ATerm)v.elementAt(1));
	    if (! (argSorts).isEmpty()) {
		pvsspec.append("["+transID(argSorts.getFirst()));
		argSorts=argSorts.getNext();
		while (! argSorts.isEmpty()) {
		    pvsspec.append(","+transID(argSorts.getFirst()));
		    argSorts=argSorts.getNext();
		}
		pvsspec.append("->"+resultSort+"]");
	    } else pvsspec.append (resultSort);
	} else System.out.println("Error - Partial function");//debug
	
	
    }

    void transSORTS(ATerm sorts) {
	ATermList sortlist=(ATermList)sorts.match("sorts(SORT*(<term>))").elementAt(0);;
	if (!(sortlist.isEmpty())) {
	    pvsspec.append(transID(sortlist.getFirst()));
	    sortlist=sortlist.getNext();
	    while (!(sortlist.isEmpty())) {
		pvsspec.append(","+transID(sortlist.getFirst()));
		sortlist=sortlist.getNext();
	    }
	}
	
    }

    // if rec is true transOP_HEAD inserts a 'RECURSIVE' keyword
    void transOP_HEAD(ATerm op_head,boolean rec) {
	if (((ATermAppl)op_head).getName()=="total-op-head") {
	    Vector v=op_head.match ("total-op-head(<term>,<term>)");
	    transARG_DECL((ATerm)v.elementAt(0));
	    ATerm sort=(ATerm)v.elementAt(1);
	    pvsspec.append(":");
	    if (rec) {pvsspec.append("RECURSIVE ");}
	    pvsspec.append(transID(sort));
	} else System.out.println("Error = partial function");
		
    }    
    
    // transArg_DECL deals with an ATermList of arg-decls for an op-defn or pred-defn
    void transARG_DECL(ATerm arg_decl) {
	ATermList ad = (ATermList)arg_decl.match("ARG-DECL*(<term>)").elementAt(0);
	if (! ad.isEmpty()) {
	    pvsspec.append("(");
	    while (!(ad.isEmpty())) {
		ATerm a=ad.getFirst();
		Vector v=a.match("arg-decl(VAR+(<term>),<term>)");
		ATermList varlist=(ATermList) v.elementAt(0);
		if (! varlist.isEmpty()) {
		    pvsspec.append(transID(varlist.getFirst()));
		    varlist=varlist.getNext();
		    while (! varlist.isEmpty()) {
			pvsspec.append(","+transID(varlist.getFirst()));
			varlist=varlist.getNext();			
		    }
		}
		pvsspec.append(":"+ transID((ATerm)v.elementAt(1)));
		ad=ad.getNext();
		if (! ad.isEmpty()) {pvsspec.append(",");}

	    }
	    pvsspec.append(")");
	}
    }
    void transPRED_ITEMS(ATerm pred_items) {
	ATermList pd=(ATermList)pred_items.match("PRED-ITEM+(<term>)").elementAt(0);

	while (!(pd.isEmpty())) {
	    ATermAppl a=(ATermAppl)pd.getFirst();

	    // predicate declarations
	    if (a.getName()=="pred-decl" ){
		Vector v=a.match("pred-decl(PRED-NAME+(<term>),<term>)");
		ATermList nameList=(ATermList)v.elementAt(0);
		pvsspec.append(transID(nameList.getFirst()));
		nameList=nameList.getNext();
		while (! nameList.isEmpty()) {
		    pvsspec.append(","+transID(nameList.getFirst()));
		    nameList=nameList.getNext();
		}
		pvsspec.append(":");
		transPRED_TYPE((ATerm)v.elementAt(1));
		pvsspec.append ("\n");
		
		//predicate definitions
	    } else if (a.getName()=="pred-defn") {
		// NB recursive predicates are dealt with differently here
		// from my write-up

		// rec determines whether a 'RECURSIVE' keyword should be used
		// in the PRED_HEAD
		boolean rec=false;
		Vector v=a.match("pred-defn(<term>,<term>,<term>)");
		StringBuffer measure = new StringBuffer();
		pvsspec.append(transID((ATerm)v.elementAt(0)));
		if (isRecursive((ATerm)v.elementAt(0),(ATerm)v.elementAt(2))) {
		    measure = measure.append("MEASURE "+
					     getMeasure((ATerm)v.elementAt(1))+"\n");
		    rec=true;
		}

		transPRED_HEAD((ATerm)v.elementAt(1),rec);
		pvsspec.append("=");
		transFORMULA((ATerm)v.elementAt(2));
		pvsspec.append("\n"+measure);
	    } else System.out.println("Error incorrect Pred-Item name "+a.getName());//debug
	    pd=pd.getNext();
	}
    }

    void transPRED_TYPE(ATerm pred_type) {
	ATerm sorts=(ATerm)pred_type.match("pred-type(<term>)").elementAt(0);
	pvsspec.append("[");
	transSORTS(sorts);
	pvsspec.append("->bool]");
    }
    
    // if rec is set to 'true' a 'RECURSIVE' keyword is inserted.
    void transPRED_HEAD(ATerm pred_head, boolean rec) {
	Vector v = pred_head.match("pred-head(<term>)");
	transARG_DECL((ATerm)v.elementAt(0));
	pvsspec.append(":");
	if (rec) {pvsspec.append("RECURSIVE ");}
	pvsspec.append("bool");
	
    }

    //transDATATYPE_DECL adds datatype names and constructors to datatypes hashtable
    String transDATATYPE_DECL(ATerm datatype_decl) {
	Vector v=datatype_decl.match("datatype-decl(<term>,ALTERNATIVE+(<term>))");
	String name = transID((ATerm)v.elementAt(0));
	ATermList altlist=(ATermList) v.elementAt(1);
	datatypes.put(name,altlist);
	return name;
    }

    void transVAR_DECL(ATerm var_decl, boolean isdecl) {
	Vector v=var_decl.match("var-decl(VAR+(<term>),<term>)");
	ATermList varlist=(ATermList)v.elementAt(0);
	if (! varlist.isEmpty()) {
	    pvsspec.append(transID(varlist.getFirst()));
	    varlist=varlist.getNext();
	    while (! varlist.isEmpty()) {
		pvsspec.append(","+transID(varlist.getFirst()));
		varlist=varlist.getNext();
	    }
	}
	pvsspec=pvsspec.append(":");
	if(isdecl){
	    pvsspec.append("VAR ");
	}
	pvsspec=pvsspec.append(transID((ATerm)v.elementAt(1)));
    }
 
    void transFORMULA (ATerm formula) {
	String name = ((ATermAppl)formula).getName();
	if (name=="quantification") {
	    Vector v = formula.match("quantification(<term>,VAR-DECL+(<term>),<term>)");
	    //transQUANTIFIER((ATerm)v.elementAt(0));

	    ATermAppl quant=(ATermAppl)v.elementAt(0);
	    ATermList vardecls=(ATermList)v.elementAt(1);
	    ATerm form=(ATerm)v.elementAt(2);

	    if (quant.getName()=="exists-uniquely") {
		pvsspec.append("EXISTS");
		pvsspec.append("(");
		for (int i=0;i<vardecls.getLength();i++) {
		    transVAR_DECL(vardecls.elementAt(i),false);
		    if (i<vardecls.getLength()-1) {
			pvsspec.append(",");
		    }
		}
		pvsspec.append("):");
		transFORMULA(form);
		pvsspec.append(" AND FORALL (");
		int varno=1;
		for (int i=0;i<vardecls.getLength();i++) {
		    ATerm a=vardecls.elementAt(i);
		    Vector w=a.match("var-decl(VAR+(<term>),<term>)");
		    int n=((ATermList)w.elementAt(0)).getLength();
		    for (int j=0;j<n;j++) {
			pvsspec.append("x"+varno);
			varno++;
			if (j<n-1) {
			    pvsspec.append(",");
			}
		    }
		    pvsspec.append(":"+transID((ATerm)w.elementAt(1)));
		    if (i<vardecls.getLength()-1) {
			pvsspec.append(",");
		    }
		}
		pvsspec.append("): (LAMBDA (");
		for (int i=0;i<vardecls.getLength();i++) {
		    transVAR_DECL(vardecls.elementAt(i),false);
		    if (i<vardecls.getLength()-1) {
			pvsspec.append(",");
		    }
		}
		pvsspec.append("): ");
		transFORMULA (form);
		pvsspec.append(")(");
		for (int i=1;i<varno;i++) {
		    pvsspec.append("x"+i);
		    if (i<varno-1) {
			pvsspec.append(",");
		    }
		}
		pvsspec.append(") IMPLIES (");
		
		
		for (int i=0;i<vardecls.getLength();i++) {
		    transVAR_DECL(vardecls.elementAt(i),false);
		    if (i<vardecls.getLength()-1) {
			pvsspec.append(",");
		    }
		}
		
		pvsspec.append(")=(");
		for (int i=1;i<varno;i++) {
		    pvsspec.append("x"+i);
		    if (i<varno-1) {
			pvsspec.append(",");
		    }
		}
		pvsspec.append(")\n");
		
	    } else {
		if (quant.getName()=="forall"){
		    pvsspec.append("FORALL "); 

		} else if (quant.getName()=="exists") {
		    pvsspec.append("EXISTS ") ;
		
		} else pvsspec.append("ERROR - incorrect quantifier" +quant.getName());//debug
	    
		pvsspec.append("(");
	    
		while (! vardecls.isEmpty()) {
		    transVAR_DECL(vardecls.getFirst(),false);
		    vardecls=vardecls.getNext();
		    if (! vardecls.isEmpty()) pvsspec.append(",");
		}
		pvsspec.append("): ");
		transFORMULA(form);
	    }

	} else if (name=="conjunction") {
	    Vector v=formula.match("conjunction(FORMULA+(<term>))");
	    ATermList flist = (ATermList) v.elementAt(0);
	    if (! flist.isEmpty()) {
		pvsspec.append("(");
		transFORMULA(flist.getFirst());
		flist=flist.getNext();
		while (! flist.isEmpty()) {
		    pvsspec.append(" AND ");
		    transFORMULA(flist.getFirst());
		    flist=flist.getNext();
		}
	       pvsspec.append(")");
	    }
	    
	} else if (name=="disjunction") {
	    Vector v=formula.match("disjunction(FORMULA+(<term>))");
	    ATermList flist = (ATermList) v.elementAt(0);
	    if (! flist.isEmpty()) {
		pvsspec.append("(");
		transFORMULA(flist.getFirst());
		flist=flist.getNext();
		while (! flist.isEmpty()) {
		    pvsspec.append(" OR ");
		    transFORMULA(flist.getFirst());
		    flist=flist.getNext();
		}
		pvsspec.append(")");
	    }
	    
	} else if (name=="implication") {
	    Vector v=formula.match("implication(<term>,<term>)");
	    pvsspec.append("(");
	    transFORMULA((ATerm)v.elementAt(0));
	    pvsspec.append("=>");
	    transFORMULA((ATerm)v.elementAt(1));
	    pvsspec.append(")");
	    
	} else if (name=="equivalence") {
	    Vector v=formula.match("equivalence(<term>,<term>)");
	    pvsspec.append("(");
	    transFORMULA((ATerm)v.elementAt(0));
	    pvsspec.append("<=>");
	    transFORMULA((ATerm)v.elementAt(1));
	    pvsspec.append(")");
	    
	} else if (name=="negation") {
	    Vector v=formula.match("negation(<term>)");
	    pvsspec.append("NOT ");
	    transFORMULA((ATerm)v.elementAt(0));
	    
	} else if (name=="true") {
	    pvsspec.append("TRUE");

	} else if (name=="false") {
	    pvsspec.append("FALSE");

	} else if (name=="predication") {
	    Vector v=formula.match("predication(<term>,<term>)");
	    transPRED_SYMB((ATerm) v.elementAt(0));
	    pvsspec.append("(");
	    ATermList termlist =(ATermList)((ATerm)v.elementAt(1)).
		match("terms(TERM*(<term>))").elementAt(0);
	    if (! termlist.isEmpty()) {
		transTERM(termlist.getFirst());
		termlist=termlist.getNext();
		while (! termlist.isEmpty()) {
		    pvsspec.append(",");
		    transTERM (termlist.getFirst());
		    termlist=termlist.getNext();
		}
		pvsspec.append(")");
	    }

	} else if (name=="definedness") {
	    //Only relevent for partial functions, so not included here.
	
	} else if (name=="strong-equation"|name=="existl-equation") {
	    //these are the same for total functions
	    
	    ATermList v=((ATermAppl)formula).getArguments();
	    pvsspec.append("(");
	    transTERM (v.elementAt(0));
	    pvsspec.append("=");
	    transTERM (v.elementAt(1));
	    pvsspec.append(")");

	} else if (name=="membership") {
	    //don't know how to do this
	    
	} else System.out.println("ERROR - incorrect formula name"+name);//debug
    
    }
    	     

    void transPRED_SYMB (ATerm pred_symb) {
    	if (((ATermAppl)pred_symb).getName()=="PRED-NAME") {
	    ATerm id = (ATerm) (pred_symb.match("PRED-NAME(<term>)")).elementAt(0);
	    pvsspec.append(transID(id));
			   
	} else if (((ATermAppl)pred_symb).getName()=="qual-pred-name") {
	    ATerm id = (ATerm) (pred_symb.match("qual-pred-name(<term>,<term>)")).elementAt(0);
	    pvsspec.append(transID(id));
	} else pvsspec.append ("ERROR - incorrect PRED_SYMB"+((ATermAppl)pred_symb).getName());//debug
    }



    void transTERMS(ATermList termlist) {
	if (! termlist.isEmpty()) {
	    transTERM(termlist.getFirst());
	    termlist=termlist.getNext();
	    while (! termlist.isEmpty()) {
		pvsspec.append(",");
		transTERM(termlist.getFirst());
		termlist=termlist.getNext();
	    }
	}
    }
    
    void transTERM(ATerm term) {
	String name=(((ATermAppl)term).getName());
	if (name=="ID") {
	    ATerm id=(ATerm)(term.match("ID(<term>)")).elementAt(0);
	    pvsspec.append(transID (id));
	    
	} else if (name=="qual-var") {
	    Vector v=term.match("qual-var(<term>,<term>)");
	    pvsspec.append(transID((ATerm)v.elementAt(0))+":"
				   + transID((ATerm)v.elementAt(1)));

	} else if (name=="application") {
	    Vector v=term.match("application(<term>,terms(TERM*(<term>)))");
	    transOP_SYMB ((ATerm)v.elementAt(0));
	    ATermList args = (ATermList)v.elementAt(1);
	    if (! args.isEmpty()) {
		pvsspec.append("(");
		transTERMS (args);
		pvsspec.append(")");
	    }

	} else if (name=="sorted-term") {
	    Vector v=term.match("sorted-term(<term>,<term>)");
	    transTERM((ATerm)v.elementAt(0));
	    pvsspec.append(":"+transID((ATerm)v.elementAt(1)));
	    
	} else if (name=="cast") {
	    Vector v=term.match("cast(<term>,<term>)");
	    transTERM((ATerm)v.elementAt(0));
	    pvsspec.append(":"+transID((ATerm)v.elementAt(1)));
	    
	} else if (name=="conditional") {
	    Vector v=term.match("conditional(<term>,<term>,<term>)");
	    pvsspec.append("IF ");
	    transFORMULA ((ATerm)v.elementAt(1));
	    pvsspec.append(" THEN ");
	    transTERM ((ATerm)v.elementAt(0));
	    pvsspec.append(" ELSE ");
	    transTERM ((ATerm)v.elementAt(2));
	    pvsspec.append(" ENDIF");
	} else System.out.println("ERROR - incorrect term name"+name);//debug
    }

    void transOP_SYMB (ATerm op_symb) {
	if (((ATermAppl)op_symb).getName()=="OP-NAME") {
	    ATerm id = (ATerm) (op_symb.match("OP-NAME(<term>)")).elementAt(0);
	    pvsspec.append(transID(id));
			   
	} else if (((ATermAppl)op_symb).getName()=="qual-op-name") {
	    ATerm id = (ATerm) (op_symb.match("qual-op-name(<term>,<term>)")).elementAt(0);
	    pvsspec.append(transID(id));

	} else pvsspec.append ("ERROR - incorrect OP_SYMB"+((ATermAppl)op_symb).getName());//debug
    }
	
    String transID(ATerm id) {
	StringBuffer s=new StringBuffer();
	String idType = ((ATermAppl)id).getName();
	if (idType=="SIMPLE-ID") {
	    Vector v=id.match("SIMPLE-ID(WORDS(<term>))");
	    s = s.append(((ATermAppl)v.elementAt(0)).getName());
	
	} else if (idType=="ID") {
	    Vector v=id.match("ID(<term>)");
	    ATermAppl id2 = (ATermAppl)v.elementAt(0);
	    s.append(transID(id2));
	
	} else if (idType=="TOKEN-ID") {
	    Vector v=id.match("TOKEN-ID(TOKEN(WORDS(<term>)))");
	    s.append(((ATermAppl)v.elementAt(0)).getName());

	    // MIXFIX-ID's are dealt with by ignoring the places and bunching the tokens
	    // together.  Invisible identifiers, consisting of places only, are not supported
	} else if (idType=="MIXFIX-ID") {
	    Vector v=id.match("MIXFIX-ID(token-places(TOKEN-OR-PLACE+(<term>)))");
	    ATermList TP=(ATermList) v.elementAt(0);
	    while (! TP.isEmpty()) {
		ATermAppl a = (ATermAppl)TP.getFirst();
		if (a.getName()=="TOKEN") {
		    Vector w=a.match("TOKEN(<term>)");
		    ATermAppl n=(ATermAppl)(((ATermAppl)w.elementAt(0)).getArgument(0));
		    s.append(n.getName());
		    TP=TP.getNext();
		} else if (a.getName()=="__") {
		    TP=TP.getNext();
		} else System.out.println("Incorrect Token-or-Place");//debug
	    }
	} else System.out.println("Incorrect ID type "+id);
	    
	    
	return s.toString();
    }

    // This function checks if the name of an operation or predicate is included in
    // the term defining it.  Therefore it doesn't support overloading.
    boolean isRecursive(ATerm name, ATerm term) {
	boolean result = false;
	int t = term.getType();
	switch (t) {
	case 3:
	    Vector v = term.match("OP-NAME(<term>)");
	    Vector u = term.match("PRED-NAME(<term>)");

	    if (v!=null) {
		if (name.isEqual((ATerm)v.elementAt(0))) {
		    return true;
		}
	    }
	    if (u!=null) {
		if (name.isEqual((ATerm)u.elementAt(0))) {
		    return true;
			}
	    }
	    ATerm listargs = ((ATermAppl)term).getArguments();
	    result = isRecursive(name, listargs);
	    return result;

	case 4:
	    ATermList termlist=(ATermList)term;
	    while (! termlist.isEmpty()) {
		if (isRecursive (name, termlist.getFirst())) {
		    return true;
		}
		termlist=termlist.getNext();
	    }
	    return false;
	    
        default:
	    System.out.println("incorrect type in 'isRecursive'");//debug
	    return result;
	}
    }

    // For a recursive operation or predicate this function puts together the actual
    // measure required from the measures generated for each free datatype among the
    // arguments.
    String getMeasure (ATerm op_head) {
	Vector v = new Vector();	
	if (((ATermAppl)op_head).getName()=="total-op-head") {
	    v=op_head.match("total-op-head(ARG-DECL*(<term>),<term>)");
	}
	
	if (((ATermAppl)op_head).getName()=="pred-head") {
	    v=op_head.match("pred-head(ARG-DECL*(<term>))");
	}

	StringBuffer m = new StringBuffer("(LAMBDA (");//actual measure
	Vector args = new Vector();
	ATermList a = (ATermList)v.elementAt(0);
	int argNo=1;
	while (! a.isEmpty()) {
	    Vector u = (a.getFirst()).match("arg-decl(VAR+(<term>),<term>)");
	    String type = transID((ATerm)u.elementAt(1));
	    ATermList b=(ATermList)u.elementAt(0);
	    while (! b.isEmpty()) {
		args.addElement(type);
		m=m.append("x"+argNo);
		argNo++;
		b=b.getNext();
		if (! b.isEmpty()) {m=m.append(",");}
	    }
	    m=m.append(":"+type);
	    a=a.getNext();
	    if (! a.isEmpty()) {m=m.append(",");}
	}
	m=m.append("): ");
	argNo=1;
	
	while (! args.isEmpty()) {
	    
	    if (datatypes.containsKey(args.elementAt(0))) {
		m=m.append((String)datatypes.get(args.elementAt(0))+"(x"+argNo+")+");
	    }
	    
	    args.removeElementAt(0);

	    argNo++;
	    }

	   
	    m=m.append("0)");
	    return m.toString();
    }
}