package code.lang; import code.instr.*; import code.modules.CurryModule; import code.space.Client; import code.space.Computation; import code.space.ComputationFactory; import code.stuff.Logger; import code.stuff.Tracer; import code.subst.Subst; import code.subst.VarSubst; import code.symbols.*; import code.table.ModuleTable; import code.term.Term; import code.term.Variable; import code.term.visitor.OccurCheckTermVisitor; import code.type.*; import static code.type.PredefinedTypes.*; import static code.type.TypeFactory.*; import java.util.Vector; /** * This class implements the "success" module. It also implements a "Fail" * constructor of some poorly-understood singleton datatype. The following * symbols are defined: 
 * Fail               Constructor (overloaded for any type)
 * failed             operation that evaluates to Fail
 * Success            Constructor (private in Curry)
 * success            operation that evaluates to Success
 * =:=                constrained strict equality (overloaded)
 * &, &>              parallel and sequential constrained conjunctions
 *
* * @author Sergio Antoy * @since Feb 28, 2003 */ public class SuccessModule extends CurryModule { // public static final String moduleName = "$Success"; public static final String moduleName = "Prelude"; /** * Constructor for the SuccessModule object */ public SuccessModule() { super(moduleName, new Vector(), null, 0,createSymbols(), false); } /** * Description of the Method * * @return Description of the Return Value */ private static Vector createSymbols() { Vector v = new Vector(); v.add(successTypeSymbol); v.add(failConstructor); v.add(failedOperation); v.add(successConstructor); v.add(successOperation); v.add(constrainedEq); v.add(paraConstrained); return v; } private final static TypeSymbol successTypeSymbol = new TypeSymbol(moduleName, successTypeName, 0, Symbol.Public); // ------------------------------------------------------------------ /** * This should be the only constructor with kind=Symbol.Failure. Every * other constructor of every other type should have a kind greater than * Symbol.Failure. */ public final static String failConstructorName = "Fail"; private final static DataSymbol failConstructor = new ConstructorSymbol(moduleName, failConstructorName, DataSymbol.toplevel, 0, DataSymbol.Failure, DataSymbol.NonInfix, DataSymbol.NonInfix, Symbol.Public, successType); public final static Term termFail = new Term(ModuleTable.getId(moduleName, failConstructorName), new Term[]{}); // ------------------------------------------------------------------ // Function returning Fail. Cannot be compiled in Curry. private final static DataSymbol failedOperation = new OperationSymbol(moduleName, "failed", DataSymbol.toplevel, 0, DataSymbol.NonInfix, DataSymbol.NonInfix, Symbol.Public, successType, new Instruction[]{ new MakeTerm(moduleName, failConstructorName), Pop.singleton, Replace.singleton, }); // ------------------------------------------------------------------ // Constructor of the singleton type Success. // Cannot be compiled in Curry. private final static String successConstructorName = "Success"; private final static DataSymbol successConstructor = new ConstructorSymbol(moduleName, successConstructorName, DataSymbol.toplevel, 0, DataSymbol.Failure + 1, DataSymbol.NonInfix, DataSymbol.NonInfix, Symbol.Public, successType); public final static Term successTerm = new Term(ModuleTable.getId(moduleName, successConstructorName), new Term[]{}); // ------------------------------------------------------------------ // Function returning Success. Cannot be compiled in Curry. private final static DataSymbol successOperation = new OperationSymbol(moduleName, "success", DataSymbol.toplevel, 0, DataSymbol.NonInfix, DataSymbol.NonInfix, Symbol.Public, successType, new Instruction[]{ new MakeTerm(moduleName, successConstructorName), Pop.singleton, Replace.singleton, }); // ------------------------------------------------------------------ // Constrained equality. Cannot be compiled in Curry. /** * Description of the Class * * @author jimeng * @since June 17, 2003 */ private static class EqSuccessCode implements Instruction { public void execute(Computation computation) { Term term = computation.getTerm(); if (Tracer.instruction) { Logger.logln(computation.getIdString() + ": Builtin " + term); } Term left = term.getArgument((byte) 0); Term right = term.getArgument((byte) 1); switch (left.getKind()) { case DataSymbol.Operation: computation.push(left); break; case DataSymbol.Failure: term.update(termFail); break; case DataSymbol.UnboundVariable: switch (right.getKind()) { case DataSymbol.Operation: computation.push(right); break; case DataSymbol.Failure: term.update(termFail); break; case DataSymbol.UnboundVariable: // TODO: some code in bindAndRestart could be moved // here to slightly improve efficiency bindAndRestart((Variable) left.getRepresentation(), right, computation); break; default: // right is constructor-rooted bindAndRestart((Variable) left.getRepresentation(), right, computation); break; } break; default: // left is constructor-rooted switch (right.getKind()) { case DataSymbol.Operation: computation.push(right); break; case DataSymbol.Failure: term.update(termFail); break; case DataSymbol.UnboundVariable: bindAndRestart((Variable) right.getRepresentation(), left, computation); break; default: // both left and right are constructor-rooted Term reduct = left.eqSuccess(right); if (Tracer.reduction) Tracer.traceRewrite(computation, term, reduct); term.update(reduct); } } } // Isn't this ugly ??? // Since variables kill computations, // dynamic polymorphism seems inconvenient. private void bindAndRestart (Variable variable, Term otherSide, Computation computation) { Term term = computation.getTerm(); if (otherSide.getRepresentation() == variable) { term.update(SuccessModule.successTerm); } else if (OccurCheckTermVisitor.singleton.checkOccur(otherSide, variable)) { if (Tracer.computation) { Logger.logln("-C- " + computation.debug() + " occurcheck " + variable + " in " + otherSide); } Term reduct = SuccessModule.termFail; if (Tracer.computation) { Logger.logln("-C- " + computation.debug() + " replacing " + term + " with " + reduct); } term.update(reduct); computation.selfSetState(Computation.FAILED); } else { // otherSide is a HNF // if it is a primitive type, it is a NF too. Term binding; if (otherSide.isNF()) { binding = otherSide; } else { // THIS IS TERRIBLY INEFFICIENT ??? int root = otherSide.getRoot(); Term[] argument = new Term[otherSide.getArgument().length]; for (int i = 0; i < argument.length; i++) { argument[i] = new Term(new Variable()); } binding = new Term(root, argument); } if (Tracer.computation) { Logger.logln("-C- " + computation.debug() + " binding " + binding + " to " + variable); } Subst subst = new VarSubst(variable, binding, computation.getSubst()); computation.selfSetState(Computation.ABANDONED); Computation top = computation.getTop(); Client client = top.client; Term topLevel = top.getResult(); Term newTerm = topLevel.cloneWithSubst(subst); if (Tracer.reduction) { Logger.logln(computation.getIdString() + " NAR " + topLevel + " => " + newTerm); } ComputationFactory.create(newTerm, subst, client); } } public String printAsTxtLoadable() { return "Constrained equality -- primitive"; } } //a -> a -> Success private final static DataSymbol constrainedEq = new OperationSymbol(moduleName, "=:=", DataSymbol.toplevel, 2, DataSymbol.NonAssoc, 4, Symbol.Public, makeFunctionType (makeTypeVariable("a"), makeFunctionType (makeTypeVariable("a"), successType)), new Instruction[]{ new EqSuccessCode() } ); // ------------------------------------------------------------------ // Paralled constrained and. Cannot be compiled in Curry. /** * Description of the Class * * @author jimeng * @since June 17, 2003 */ private static class ParallelAndCode implements Instruction { private final static byte LEFT = 0; private final static byte RIGHT = 1; /** * Description of the Method * * @param computation Description of the Parameter */ public void execute(Computation computation) { Term term = computation.getTerm(); // must be &-rooted if (Tracer.instruction) { Logger.logln(computation.getIdString() + ": Builtin " + term); } computation.selfSetState(Computation.WAITING); Subst subst = computation.getSubst(); Computation left = ComputationFactory.create (term.getArgument(LEFT), subst, computation); Computation right = ComputationFactory.create (term.getArgument(RIGHT), subst, computation); right.selfSetState(Computation.WAITING); computation.setChildren(new Computation[]{left, right}); } public String printAsTxtLoadable() { return "Parallel AND -- primitive"; } } private final static DataSymbol paraConstrained = new OperationSymbol(moduleName, "&", DataSymbol.toplevel, 2, DataSymbol.Right, 0, Symbol.Public, makeFunctionType(successType, makeFunctionType(successType, successType)), new Instruction[]{ new ParallelAndCode() } ); }