Function Rewrite

rewrite/rewrite.go:36–63

Rewrite transforms each clause of a given layer (stratum) of a program to another one where transforms only appear on clauses with a single atom that defines all variables.

(stratum analysis.Program)

// Rewrite transforms each clause of a given layer (stratum) of a program to another one where
// transforms only appear on clauses with a single atom that defines all variables.
func Rewrite(stratum analysis.Program) analysis.Program {
	gen := freshNameGenerator()

	var newRules []ast.Clause
	for _, clause := range stratum.Rules {
		if (clause.Transform == nil) || clause.Transform.IsLetTransform() || isSingleAtomPremise(clause.Premises) {
			newRules = append(newRules, clause)
			continue
		}

		// Make a new predicate that captures all variables.
		p := clause.Head.Predicate

		vars := make(map[ast.Variable]bool)
		for _, premise := range clause.Premises {
			getVars(premise, vars)
		}
		// Wildcard variables _ do not correspond to any column in the result relation.
		delete(vars, ast.Variable{"_"})

		internalPred := gen.freshPredicateName(p, len(vars))

		newHead := makeHead(internalPred, vars)
		newRules = append(newRules, ast.Clause{newHead, nil, clause.Premises, nil})
		newRules = append(newRules, ast.Clause{clause.Head, clause.HeadTime, []ast.Term{newHead}, clause.Transform})
	}
	return analysis.Program{stratum.EdbPredicates, stratum.IdbPredicates, newRules}
}

type nameGen struct {
	n int