package ws.prova.reference;

/*
 * Copyright (C) 1999-2006 <a href="mailto:adrian.paschke@gmx.de">Adrian Paschke</a>
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

import org.mandarax.kernel.*;
import org.mandarax.reference.DefaultSemanticEvaluationPolicy;
import org.mandarax.reference.RobinsonsUnificationAlgorithm;
import org.mandarax.reference.SemanticEvaluationPolicy;
import org.mandarax.util.StringUtils;
import ws.prova.kernel.ProvaTerm;
import rbsla.owl.OWL2PROVA;

import java.util.*;

/**
 * Reference implementation of Robinson's unification algorithm.
 *
 * @author <A HREF="mailto:paschke@gmx.de">Adrian Paschke</A>
 * @author <A HREF="mailto:mandarax@jbdietrich.com">Jens Dietrich</A>
 * @author <A HREF="mailto:a.kozlenkov@city.ac.uk">Alex Kozlenkov</A>
 * @version 0.1 <15 Dec 2005>
 * @since 0.1
 *
 * <p>ContractLogs' hybrid typed unification for Semantic Web (description logic DL) type systems (RDFS / OWL Lite / OWL DL)
 * Extends the Prova Java-typed logic with a hybrid DL-typed logic</p>
 * <p>Untyped variables can be either unified with Java or DL-typed variables</p>
 * <p>For hybrid DL reasoning the ContractLog rbsla.owl.OWL2PROVA framework is used.
 * <p>The following predefined reasoners can be used (see OWL2PROVA):
 * <ul><li>  "" | "empty" | null = no reasoner
 * <li>  default = OWL reasoner
 * <li>  transitive = transitive reasoner
 * <li>  rdfs = RDFS rule reasoner
 * <li>  owl = OWL reasoner
 * <li>  daml = DAML reasoner
 * <li>  dl = OWL-DL reasoner (uses pellet)
 * <li>  swrl = SWRL reasoner (uses pellet)
 * <li>  rdfs_full = rdfs full reasoner
 * <li>  rdfs_simple = rdfs simple reasoner
 * <li>  owl_mini = owl mini reasoner
 * <li>  owl_micro = owl micro reasoner
 * </ul>
 * User-defined reasoners can be set (<code>OWL2PROVA.setReasoner</code>).
 * Dependencies: rbsla.owl.OWL2PROVA
 * </p>
 * 
 */
public final class RBSLARobinsonsUnificationAlgorithm extends RobinsonsUnificationAlgorithm {

	List substitutions = new LinkedList();
	List substitutionsLocal = new LinkedList();
	List subterms1 = new ArrayList();
	List subterms2 = new ArrayList();
	
	// DL typing variables
	private String reasoner;   // the reasoner used for DL reasoning
	private List typeURIs; // a list of URIs pointing to external type systems

	private SemanticEvaluationPolicy semanticEvaluationPolicy = new DefaultSemanticEvaluationPolicy();

	/**
	 * Constructor.
	 */
	public RBSLARobinsonsUnificationAlgorithm() {		
		super();
		reasoner="default"; // default reasoner
		typeURIs = new ArrayList(); // no external DL type system
	}
	
	/**
	 * Constructor.
	 * @param _reasoner the reasoner for DL reasoning
	 * @param typeURI an URI (String representation) pointing to an external DL type systems (RDFS / OWL files)
	 * 
	 */
	public RBSLARobinsonsUnificationAlgorithm(String _reasoner, String typeURI) {		
		super();
		reasoner=_reasoner;
		typeURIs = new ArrayList();
		typeURIs.add(typeURI);
	}
	
	/**
	 * Constructor.
	 * @param _reasoner the reasoner for DL reasoning
	 * @param _typeURIs a list of URIs pointing to external DL type systems (RDFS / OWL files)
	 * 
	 */
	public RBSLARobinsonsUnificationAlgorithm(String _reasoner, List _typeURIs) {		
		super();
		reasoner=_reasoner;
		typeURIs = _typeURIs;
	}
	
	/**
	 * Set the external reasoner for DL typing
	 * @param _reasoner
	 */
	public void setReasoner(String _reasoner) {
		reasoner = _reasoner;
	}
	
	/**
	 * Get the external reasoner for DL typing
	 * @return reasoner name
	 */
	public String getReasoner() {
		return reasoner;
	}
	
	/**
	 * Add an URI pointing to an external DL type system (RDFS / OWL file) 
	 * @param typeURI String representation of URI
	 */
	public void addTypeURI(String typeURI) {
		typeURIs.add(typeURI);
	}
	
	/**
	 * Remove an external DL type system from the imported type systems
	 * @param typeURI
	 */
	public void removeTypeURI(String typeURI) {
		typeURIs.remove(typeURI);
	}
	
	/**
	 * Get list of imported external DL type systems
	 * @return List of URIs pointing to external DL type systems
	 */
	public List getTypeURIs() {
		return typeURIs;
	}

    /**
     * Make sure the substitutions are freed before proceeding to the next recursion level.
     * Called from ResolutionInferenceEngine5
     */
    public void renewSubstitutions() {
        substitutions.clear();
        substitutionsLocal.clear();
    }

    /**
	 * An optimized version of collecting subterms of an array of terms.
	 *
	 * @param terms  Term[] an array of terms to look for subterms in.
	 * @param result List
	 */
	private void getAllSubtermsA(final Term[] terms, final List result) {
		result.clear();
		for (int i = 0; i < terms.length; i++) {
			terms[i].getAllSubtermsA(result);
		}
	}

	/**
	 * Unify the two arrays of terms. Return <code>Unification.noUnificationPossible</code> if unifiction fails.
	 *
	 * @param t1      the first array of terms
	 * @param t2      the second array of terms
	 * @param session a session
	 * @return the computed unification
	 * @see org.mandarax.kernel.Unification#noUnificationPossible
	 */
	public Unification unify(Term[] t1, Term[] t2, Session session) {
		List substitutions = new ArrayList();
		boolean logOn = LOG_IE_UNIFICATION.isDebugEnabled();

		if (logOn) {
			LOG_IE_UNIFICATION.debug("Trying to unify: "
					+ StringUtils.toString(t1) + " and "
					+ StringUtils.toString(t2));
		}

		return unify(t1, t2, substitutions, 0, session, logOn);
	}

	/**
	 * Unify two arrays of terms.
	 *
	 * @param t1      the first array of terms
	 * @param t2      the second array of terms
	 * @param subst   the list of replavements
	 * @param start   start investigation at this index
	 * @param session a session
	 * @param logOn   if true then we log
	 * @return org.mandarax.kernel.Unification
	 */
	protected Unification unify(Term[] t1, Term[] t2, List subst, int start, Session session, boolean logOn) {
		Term[] subTerms1 = getAllSubterms(t1);
		Term[] subTerms2 = getAllSubterms(t2);
		int maxIdx = Math.min(subTerms1.length, subTerms2.length);
		Term subTerm1, subTerm2, original, replace;

		for (int i = start; i < maxIdx; i++) {
			original = null;
			replace = null;
			subTerm1 = subTerms1[i];
			subTerm2 = subTerms2[i];

			// find the first index to unify
			if (!subTerm1.sameAs(subTerm2)) {

				// check whether there is a variable
				if (subTerm1.isVariable()) {
					original = subTerm1;
					replace = subTerm2;
				} else if (subTerm2.isVariable()) {
					original = subTerm2;
					replace = subTerm1;
				}

				// no unification  possible if there is no variable
				if (original == null) {
					if (semanticEvaluationPolicy != null && semanticEvaluationPolicy.evaluateAndCompare(subTerm1, subTerm2, session, logOn))
						continue;
					else
						return Unification.noUnificationPossible;
				}

				// otherwise continue and enter recursion .. keep track of the index in order to not to waste time
				// investigating the same terms twice
				Replacement r = new Replacement(original, replace);
				subst.add(r);
				return unify(apply(t1, r), apply(t2, r), subst, i + 1, session, logOn);
			}
		}

		// if the algorithm is here, both terms have been unified (are equal)
		if (logOn) {
			LOG_IE_UNIFICATION.debug("Unified: " + StringUtils.toString(t1) + " and " + StringUtils.toString(t2));
			LOG_IE_UNIFICATION.debug("Substitutions:");

			for (Iterator it = subst.iterator(); it.hasNext();) {
				LOG_IE_UNIFICATION.debug(it.next().toString());
			}
		}

		return new Unification(subst, t1, t2);
	}
	
	

	/**
	 * Modified RBSLA version with additional support for DL type systems (serialized in OWL or RDFS.
	 * An external reasoner and the imported external DL type systems are used for DL typed unification.
	 * Unify the two arrays of terms. Return <code>Unification.noUnificationPossible</code> if unifiction fails.
	 *
	 * @param t1 the first array of terms
	 * @param t2 the second array of terms
	 * @return the computed unification
	 * @see org.mandarax.kernel.Unification#noUnificationPossible
	 */
	public Unification unify(final Term[] t1, final Term[] t2, final boolean isRule) {
		final Vector substitutions = new Vector();
		final Vector substitutionsLocal = new Vector();
		boolean logOn = LOG_IE_UNIFICATION.isDebugEnabled();

		if (logOn) {
			LOG_IE_UNIFICATION.debug("Trying to unify: "
					+ StringUtils.toString(t1) + " and "
					+ StringUtils.toString(t2));
		}
		
        Unification unification = unifyDL(t1, t2, substitutions, substitutionsLocal, 0, logOn, isRule);
		
        subterms1.clear();
        subterms2.clear();
		return unification;
	}


	private Unification unifyDL(final Term[] t1, final Term[] t2,
			   final List subst, final List substLocal, final int start,
			   final boolean logOn, final boolean isRule) {
		Term[] tn1 = new Term[t1.length];
		Term[] tn2 = new Term[t2.length];
		Term[] tx1 = t1;
		Term[] tx2 = t2;
		getAllSubtermsA(t1, subterms1);
		getAllSubtermsA(t2, subterms2);
		int maxIdx = Math.min(subterms1.size(), subterms2.size());
		
		Term subTerm1, subTerm2;		
		for (int i = start; i < maxIdx; i++) {
			subTerm1 = (Term) subterms1.get(i);
			subTerm2 = (Term) subterms2.get(i);			
			if (subTerm1.isCompound() && subTerm2.isCompound()) {
				// !!! Assume that all ComplexTerm-s have the same signature (true for Prova lists)			
				continue;
			}
			if (!subTerm1.sameAs(subTerm2)) {				
				boolean rc = unifyNonmatchingSubtermsDL(tn1, tn2, tx1, tx2, subTerm1,
							subTerm2, subst, substLocal,
							isRule);
				if (!rc) {
						return Unification.noUnificationPossible;
				}
		
				tx1 = tn1;
				tx2 = tn2;
				getAllSubtermsA(tx1, subterms1);
				getAllSubtermsA(tx2, subterms2);
				maxIdx = Math.min(subterms1.size(), subterms2.size());
			}
		}
		
		// if the algorithm is here, both terms have been unified (are equal)
		if (logOn) {
			LOG_IE_UNIFICATION.debug("Unified: " + StringUtils.toString(t1)
				+ " and " + StringUtils.toString(t2));
			LOG_IE_UNIFICATION.debug("Substitutions:");
			
			for (Iterator it = subst.iterator(); it.hasNext();) {
				LOG_IE_UNIFICATION.debug(it.next().toString());
			}
		}
		//System.out.println("<<<"+subst);
		//System.out.println(">>>"+substLocal);		
		return new Unification(subst, substLocal, t1, t2);
		
	}	

    /**
     * Get the DL type of the term
     * Return null if the term has no DL type
     */
    public static String getDLType(Term t) {
      try {

        String term = t.toString();
        if (term.indexOf(":")==-1)
            if (t.getType()==Object.class || t.getType()==ws.prova.RList.class) return "rdfs_Resource";
            else return null;

        else if (t.getType()==String.class || t.getType()==Object.class) {

            if (t instanceof VariableTermImpl) {
                return term.substring(term.lastIndexOf(":")+1,term.length()-1);
            } else

            if (t instanceof ConstantTermImpl) {

                //use this line if the primary type system should be DL and not Java
                //if (t.getType()==String.class) return "rdfs_Resource";

                return term.substring(1,term.indexOf(":"));
            } else

            if (t instanceof ComplexTermImpl) {
                // Complex terms are not DL typed
                return null;
            } else return null;
        }

      } catch (Exception e) {return null;}

      return null;

    }

    /*
	 * Typed unification for Java and DL type systems
	 * 	-- Object / Untyped variables are allowed to be unified with any Java objects and any ComplexTerm and any DL typed variable or individual
	 *  -- Non-object variables are only allowed to be unified with Java objects or DL variables/constants that are assignable to them 
	 *	   given their type (i.e., whose class is the same as the variable's class or its subclass)
	 *	-- RList variable unifies with any ComplexTerm
	 *  -- Complex terms are untyped and are only allowed to be unified with untyped variables (of type Object resp. rdfs_Resource)
	 */
	boolean unifyNonmatchingSubtermsDL(final Term[] tn1, final Term[] tn2,
			 final Term[] t1, final Term[] t2,
			 final Term subTerm1, final Term subTerm2,
			 final List subst, final List substLocal,
			 final boolean isRule) {
		
		
		Term original = null, replace = null;
		boolean changed1 = false, changed2 = false;
	
		if (subTerm1.isVariable()) {
			Class cl = subTerm1.getType();
			
			// variable - variable unification
						
			
			if (subTerm2.isVariable()) {
				if (subTerm2.getType() == cl || subTerm2.getType().isAssignableFrom(cl)) {					
					
					// The same classes or (1) is a subclass of (2)
																			
					Replacement rep = lower(subTerm1,subTerm2,isRule);
					
					if (rep!=null) { // DL type unification						
						original = rep.original;
						replace = rep.replacement;																	
					} else { // Java type unification
						original = subTerm2;
						replace = subTerm1;
					}
					
				} else if (cl.isAssignableFrom(subTerm2.getType())) {
					
					// (2) is a subclass of (1)
					
					Replacement rep = lower(subTerm2,subTerm1, isRule);
					
					if (rep!=null) { // DL type unification
						original = rep.original;
						replace = rep.replacement;																	
					} else { // Java type unification						
						original = subTerm1;
						replace = subTerm2;
					}
				}
			
			// variable - constant unification	
				
			} else if (subTerm2.isConstant()) {
				if (cl == Object.class || cl.isInstance(((ConstantTerm) subTerm2).getObject())) {
					Replacement rep = lower(subTerm2,subTerm1, isRule);					
					if (rep!=null) { // DL type unification						
						original = rep.original;
						replace = rep.replacement;						
					} else { // Java type unification
						original = subTerm1;
						replace = subTerm2;
					}					
				}
				
			// variable - complex unification
				
			} else if (cl == ws.prova.RList.class || cl == Object.class) {
				// subTerm2 is a ComplexTerm, unification is only possible if subTerm1 is an Object or RList variable
				// and not of DL type

                if (getDLType(subTerm1).equals("rdfs_Resource")) {
					if (((ComplexTerm) subTerm2).containsVariable((VariableTerm) subTerm1))
						return false;
					original = subTerm1;
					replace = subTerm2;
				}

			}
			
			
		} else if (subTerm2.isVariable()) {
			Class cl = subTerm2.getType();
			
			// constant - variable unification
			
			if (subTerm1.isConstant()) {
				if (cl == Object.class || cl.isInstance(((ConstantTerm) subTerm1).getObject())) {
					Replacement rep = lower(subTerm1,subTerm2, isRule);
					if (rep!=null) { // DL type unification
						original = rep.original;
						replace = rep.replacement;
					} else { // Java type unification
						original = subTerm2;
						replace = subTerm1;
					}	
				}
				
			// complex - variable unification
				
			} else if (cl == ws.prova.RList.class || cl == Object.class) {				
				// subTerm1 is a ComplexTerm, unification is only possible if subTerm2 is an Object or RList variable
				// and not DL type

                if (getDLType(subTerm2).equals("rdfs_Resource")) {
					if (((ComplexTerm) subTerm1).containsVariable((VariableTerm) subTerm2))
						return false;
					original = subTerm2;
					replace = subTerm1;
				}

			}
		}

		// no unification  possible if there is no variable
		if (original == null) {
			return false;
		}
		
		Replacement r = new Replacement(original, replace);

		for (int i1 = 0; i1 < t1.length; i1++) {
			if (t1[i1].containsVariable((VariableTerm) r.original)) {
				tn1[i1] = t1[i1].apply(r);
				changed1 = true;
				continue;
			}
			tn1[i1] = t1[i1];
		}
		
		for (int i2 = 0; i2 < t2.length; i2++) {
			if (t2[i2].containsVariable((VariableTerm) r.original)) {
				tn2[i2] = t2[i2].apply(r);
				changed2 = true;
				continue;
			}
			tn2[i2] = t2[i2];
		}
		
		if (changed1) {
			// Global substitutions affecting the goal tail should be exposed only if the goal has changed
			subst.add(r);
		}
		if (isRule && changed2) {
			// Local substitutions affecting the body of the target rule are accumulated here
			substLocal.add(r);
		}
		
		return true;
	}	

	
	public Unification unify2(final Term[] t1, final Term[] t2, boolean isRule) {
		final Vector substitutions = new Vector();
		final Vector substitutionsLocal = new Vector();
		return unifyA2(t1, t2, substitutions, substitutionsLocal, isRule);
	}
	
	
	private Unification unifyA2(final Term[] t1, final Term[] t2,
								final List subst, final List substLocal, boolean isRule) {
		if (t1.length != t2.length)
			return Unification.noUnificationPossible;
		Map vars1 = new HashMap();
		Map vars2 = new HashMap();
		for (int i = 0; i < t1.length; i++) {
			Term pt1 = ProvaTermImpl.fold(vars1, t1[i]);
			Term pt2 = ProvaTermImpl.fold(vars2, t2[i]);
//			System.out.println(vars1);
//			System.out.println(vars2);
			boolean res = ProvaTermImpl.unify(vars1, pt1, vars2, pt2);
			if (!res)
				return Unification.noUnificationPossible;
		}
//		System.out.println(vars1);
//		System.out.println(vars2);
		ProvaTermImpl.assignSubstitutions(vars1, vars2, subst, substLocal, isRule);
//		System.out.println("<<<"+subst);
//		System.out.println(">>>"+substLocal);
		return new Unification(subst, substLocal, t1, t2);
	}
	

	boolean unifyNonmatchingSubterms2(final Term[] tn1, final Term[] tn2,
									  final Term[] t1, final Term[] t2,
									  final ProvaTerm subTerm1, final ProvaTerm subTerm2,
									  final List subst, final List substLocal,
									  final boolean isRule) {
		Term original = null, replace = null;
		boolean changed1 = false, changed2 = false;


		// check whether there is a variable
		// 25/04/03: a.kozlenkov@city.ac.uk
		// Modifications to unification of typed variables with constants:
		// -- Object variables are allowed to be unified with any Java objects and any ComplexTerm
		// -- Non-object variables are only allowed to be unified with Java objects that are assignable to them
		//       given their type (i.e., whose class is the same as the variable's class or its subclass)
		// -- RList variable unifies with any ComplexTerm
		int where = 0;
		if (subTerm1.isVariable()) {
			where = 1;
			Class cl = subTerm1.getType();
			if (subTerm2.isVariable()) {
				if (subTerm2.getType() == cl || subTerm2.getType().isAssignableFrom(cl)) {
					// The same classes or (1) is a subclass of (2)
					where = 2;
					original = subTerm2;
					replace = subTerm1;
				} else if (cl.isAssignableFrom(subTerm2.getType())) {
					// (2) is a subclass of (1)
					original = subTerm1;
					replace = subTerm2;
				}
			} else if (subTerm2.isConstant()) {
				if (cl == Object.class || cl.isInstance(((ConstantTerm) subTerm2).getObject())) {
					original = subTerm1;
					replace = subTerm2;
				}
			} else if (cl == ws.prova.RList.class || cl == Object.class) {
				// subTerm2 is a ComplexTerm, unification is only possible if subTerm1 is an Object or RList variable
				if (((ComplexTerm) subTerm2).containsVariable((VariableTerm) subTerm1))
					return false;
				original = subTerm1;
				replace = subTerm2;
			}
		} else if (subTerm2.isVariable()) {
			where = 2;
			Class cl = subTerm2.getType();
			if (subTerm1.isConstant()) {
				if (cl == Object.class || cl.isInstance(((ConstantTerm) subTerm1).getObject())) {
					subTerm2.setTerm(subTerm1.getTerm());
					return true;
				}
			} else if (cl == ws.prova.RList.class || cl == Object.class) {
				// subTerm1 is a ComplexTerm, unification is only possible if subTerm2 is an Object or RList variable
				if (((ComplexTerm) subTerm1).containsVariable((VariableTerm) subTerm2))
					return false;
				original = subTerm2;
				replace = subTerm1;
			}
		}

		// no unification  possible if there is no variable
		if (original == null) {
			return false;
		}

		// otherwise continue and enter recursion .. keep track of the index in order to not to waste time
		// investigating the same terms twice
		Replacement r = new Replacement(original, replace);


//				subst.addElement (r);

//			Term[] tn1 = new Term[t1.length];
		for (int i1 = 0; i1 < t1.length; i1++) {
			if (/*where==1 || */t1[i1].containsVariable((VariableTerm) r.original)) {
				tn1[i1] = t1[i1].apply(r);
				changed1 = true;
				continue;
			}
			tn1[i1] = t1[i1];
		}
//			Term[] tn2 = new Term[t2.length];
		for (int i2 = 0; i2 < t2.length; i2++) {
			if (/*where==2 || */t2[i2].containsVariable((VariableTerm) r.original)) {
				tn2[i2] = t2[i2].apply(r);
				changed2 = true;
				continue;
			}
			tn2[i2] = t2[i2];
		}

		if (/*isRule ||*/ changed1) {
			// Global substitutions affecting the goal tail should be exposed only if the goal has changed
			subst.add(r);
		}
		if (isRule && changed2) {
			// Local substitutions affecting the body of the target rule are accumulated here
			substLocal.add(r);
		}
		return true;
	}
	

	
	
	
	/**
	 * Returns the semantic evaluation policy.
	 *
	 * @return the semantic evaluation policy
	 */
	public SemanticEvaluationPolicy getSemanticEvaluationPolicy() {
		return semanticEvaluationPolicy;
	}

	/**
	 * Sets the semantic evaluation policy.
	 *
	 * @param semanticEvaluationPolicy The semantic evaluation policy to set
	 */
	public void setSemanticEvaluationPolicy(SemanticEvaluationPolicy semanticEvaluationPolicy) {
		this.semanticEvaluationPolicy = semanticEvaluationPolicy;
	}

	
	/*
	 * Checks if the type of term t1 is a subclass or equivalent class of t2.
	 * Returns the replacement or null
	 */
	private Replacement lower(Term t1, Term t2, boolean isRule) {

		if (typeURIs.isEmpty()) return null; // no external DL type system available
			
		String typeDL1 = OWL2PROVA.getDLType(t1);
		String typeDL2 = OWL2PROVA.getDLType(t2);		
		if (typeDL1!=null && typeDL2!=null) { // DL type unification			
			if (typeDL2.indexOf("Resource")!=-1 && !t2.isConstant()) return new Replacement(t2,t1);
			else {								
				for (Iterator it = typeURIs.iterator();it.hasNext();) {
					try {
						String uri = (String) it.next();
						
						// (1) is subclass of (2)
						List result = OWL2PROVA.rdf(
								uri,	reasoner,
								typeDL1,"rdfs_subClassOf", typeDL2);						
						if (t1.isConstant() && result.isEmpty()) return new Replacement(null,null);
						if (!result.isEmpty()) return new Replacement(t2,t1);						
						
						// (2) is subclass of (1)
						result = OWL2PROVA.rdf(
								uri,	reasoner,
								typeDL2,"rdfs_subClassOf", typeDL1);						
						if (t2.isConstant() && result.isEmpty()) return new Replacement(null,null);
						if (!result.isEmpty()) return new Replacement(t1,t2);						
						
						// TODO: equal classes
						
					} catch (Exception e) {}
				}
			}
			return new Replacement(null,null);	// no subclass relation		
		}

		return null; // terms do not have DL type
	
	}
	
	
}
