Documentation

Node: head of lists are applied first

filterCastsByDom castList domTy. Returns all casts whose domain type |unifies with the type given, and whose range type doesn't unify with |the type given. i.e. returns a value that doesn't match the given type |from a value that does.

filterCastsByRan castList ranTy. Returns all casts whose range type |unifies with the type given, and whose domain type doesn't domain type |doesn't unify with the type given. i.e. returns a value that matches the |given type, from a value that doesn't.

Returns functions types for the casts, by getting the types of the individual |cast functions in the cast chains, and unifying the intermediate types to |get the types for the whole cast chains.

applyCasts casts expr. If there are casts for expr in casts |returns expr, with the correct chain of cast fun apps, otherwise |returns expr.

applyCast expr expId castId. Checks if the current expr's id matches |expId, and if it does returns expr nested in a function application |that calles the castId cast function.

applyCasts casts expr. Returns expr with casts inserted |as function applications.

lookupExpTy tyEnv expId. Returns the type of expId in tyEnv, |with term vars renewed. If tyEnv doesn't include expId returns |a new term var.

icCurrentAvgCost st. Returns the average cost of all currently found solutions.

CastCandidate. (CCand ast curExprIds usedCastIds cost exprId castId) |ast is current AST to apply this cast to. curExprIds are the ids of the |expressions involved in fixing the current constraint (basically the expr |ids of the originally broken expression, and all the cast fun apps applied to it). |usedCastIds is a list of the cast ids that have already been used to try and |mend the current constraint. Cost is the current cost of this candidate |(including the cost of the current cast castId that has yet to be applied to ast). |exprId is the expression the cast fun app should be applied to, and castId is |the id of the cast to apply to it. |Note: ast, curExprIds, and usedCastIds haven't had exprId and castId applied |to them yet. Only cost includes the cost of castId.

tryCandidate return codes. |1) type checks (is a solution) and so doesn't return |more candidates, 2) doesn't type check but mends current constraint and |so returns candidates to mend this next constraint, 3) doesn't type check |and doesn't mend current constraint but returns more candidates to try, |and 4) doesn't mend current constraints and no more candidates to try |i.e. cast insertion fails.

insertCasts3 curCands numPartialSols nextCands sols. Tries to insert casts in |a breadth first order, so that shorter chains of fun apps are tried before longer |ones. Tries all the candidates in curCands until there are either enough partial solutions |(numPartialSols >= maxICSols2) to start processing nextCands, or enough complete solutions |(length sols >= maxICSols2) to return. It is safe to not explore all options (i.e. |throw away curCands when we have enough partial solutions, because we know that shorter |solutions will be visited before longer ones (? is this true?). Sorting partial solutions |in order of ascending cost should ensure that the cheapest solution is always returned found first. | (Aim: to find shortest chains of redists to fix constraints before longer ones) |Problem: looking for shortest sequence of redists can lead to non-optimal solution |e.g. might use an expensive repartVMap rather than a mirrVMap.saveVMap.

tryCandidate candidate. Evaluates this candidate, to see if it is |a solution, or if it needs more casts to be applied to it.

checkSolution sol. Returns true if this solution is valid. |Currently checks if solution's types use any partition dimensions, and if |not, returns invalid, thus filtering out solutions that mirror everything.

Generates candidate solutions that might mend the current constraint, to be tried by tryCandidate.

insertCast ast castL exprId. insertCast tries to make ast's types |unify by inserting cast function applications at expressions that |break constraints. It tries to work on one expression (exprId) at a |time, until it nolonger causes a constraint failure. castL lists |the current cast function var ids that have been applied to the current |expr, so that the same cast fun isn't applied twice to a given expression. |exprId starts by refering to the expr that broke the constraint, and then |later to the highest cast func app applied to that expr.

insertCast ast castL exprId. insertCast tries to make ast's types |unify by inserting cast function applications at expressions that |break constraints. It tries to work on one expression (exprId) at a |time, until it nolonger causes a constraint failure. castL lists |the current cast function var ids that have been applied to the current |expr, so that the same cast fun isn't applied twice to a given expression. |exprId starts by refering to the expr that broke the constraint, and then |later to the highest cast func app applied to that expr.

insertCastBF ast castL exprId. Breadth first. insertCastBF tries to make ast's types |unify by inserting cast function applications at expressions that |break constraints. It tries to work on one expression (exprId) at a |time, until it nolonger causes a constraint failure. castL lists |the current cast function var ids that have been applied to the current |expr, so that the same cast fun isn't applied twice to a given expression. |exprId starts by refering to the expr that broke the constraint, and then |later to the highest cast func app applied to that expr.

findCasts funTys funIds ast. Searches for applications of cast |functions that make ast's types unify. Solutions are returned in |order of ascending cost. Works by iteratively trying to infer types |and trying to mend one constraint at a time by inserting cast functions |and then re-type-checking.

getCastFunEids exp. Returns a list of the expr ids of the (Var cast) expressions in exp.

getCastAppEids exp. Returns a list of expression ids for cast fun apps, where fst is app expr id, and snd is cast var expr id.

getExprTys tyEnv eids. Returns the types for all eids in tyEnv, throwing an error if an eid in eids is not in tyEnv.

getCastsForTy ty cands sols. Searches all chains of candidates cands in a breadth first order, to |find a chain of casts who's type will unify with ty.

All redist and relayout functions. |Note: head of lists are applied first

findCasts funTys funIds ast. Searches for applications of cast |functions that make ast's types unify. Solutions are returned in |order of ascending cost. Works by identifying places that casts are |needed by mending broken constraints by inserting cast :: a -> b. |Then gets the types inferred for these dummy casts, and searches for |chains of redist functions with types x -> y that unify with them |(e.g. a -> b :=: x -> y unifies). Then replaces these dummy casts with |these chains of functions.