<commit_before>package wyal.rules;

import java.util.IdentityHashMap;
import java.util.Map;

import wyal.heap.SyntacticHeaps;
import wyal.lang.Formula;
import wyal.lang.Proof;
import wyal.lang.SyntacticItem;
import wyal.lang.WyalFile;
import wyal.lang.Proof.State;
import wyal.lang.WyalFile.Declaration;
import wyal.lang.WyalFile.Expr;
import wyal.lang.WyalFile.Tuple;
import wyal.lang.WyalFile.Type;
import wyal.lang.WyalFile.VariableDeclaration;
import wyal.lang.WyalFile.Stmt.Block;
import wyal.util.Formulae;
import wyal.util.TypeSystem;

/**
 * <p>
 * Responsible for inlining macro invocations from their definitions. For
 * example, consider this assertion:
 * </p>
 *
 * <pre>
 * define nat(int n) is:
 *   n >= 0
 *
 * assert:
 *   forall(int x):
 *       if:
 *           x > 0
 *       then:
 *           nat(x)
 * </pre>
 * <p>
 * In proving this assertion, we will at some point come to the macro invocation
 * <code>nat(x)</code> or its <i>inversion</i> <code>!nat(x)</code>. To deal
 * with this, we simply replace <code>nat(x)</code> by its body where the
 * parameters are substituted for their arguments. That is, we replace
 * <code>nat(x)</code> by <code>n >= 0</code> and substitute <code>n</code> for
 * the argument <code>x</code>.
 * </p>
 * <p>
 * <b>NOTE:</b> A pretty obvious concern with this rule is how to deal with
 * recursive macro definitions. This has not been tried and tested at this
 * stage!
 * </p>
 *
 * @author <NAME>
 *
 */
public class MacroExpansion implements Proof.LinearRule {
	private final TypeSystem types;

	public MacroExpansion(TypeSystem types) {
		this.types = types;
	}

	@Override
	public String getName() {
		return "Macro-I";
	}

	@Override
	public State apply(Proof.State state, Formula truth) {
		Formula expanded = expandFormula(truth);
		if(expanded != null) {
			expanded = state.allocate(expanded);
			state = state.subsume(this, truth, expanded);
		}
		return state;
	}

	private Formula expandFormula(Formula formula) {
		if (formula instanceof Formula.Invoke) {
			Formula.Invoke ivk = (Formula.Invoke) formula;
			// Determine the type declaration in question
			Type.FunctionOrMacro af = ivk.getSignatureType();
			// Resolve the declaration corresponding to this invocation
			Declaration.Named decl = types.resolveAsDeclaration(ivk.getName());
			// Calculate the invariant (if any)
			Formula invariant = extractDeclarationInvariant(decl, ivk.getArguments());
			if (invariant != null) {
				if (!ivk.getSign()) {
					invariant = Formulae.invert(invariant);
				}
				// Update the state
				return Formulae.simplifyFormula(invariant,types);
			}
		} else if(formula instanceof Formula.Quantifier) {
			Formula.Quantifier quantifier = (Formula.Quantifier) formula;
			// FIXME: the basic problem is that if we have a quantifier which
			// contains a macro invocation and we don't it, then quantifier
			// instantiation won't be triggered.
		}
		return null;
	}

	private Formula extractDeclarationInvariant(Declaration.Named decl, Tuple<Expr> arguments) {
		if (decl instanceof Declaration.Named.Type) {
			// This is a type invariant macro call. In such case, we
			// need to first determine what the invariant actually is.
			Declaration.Named.Type td = (Declaration.Named.Type) decl;
			// Expand the corresponding type invariant
			return expandTypeInvariant(td, arguments.getOperand(0));
		} else if (decl instanceof Declaration.Named.Macro) {
			Declaration.Named.Macro md = (Declaration.Named.Macro) decl;
			// Expand the macro body with appropriate substitutions
			return expandMacroBody(md, arguments.getOperands());
		} else {
			// Functions are ignored
			return null;
		}<commit_msg>Bug fix for macro expansion<commit_after>package wyal.rules;

import java.util.Arrays;
import java.util.IdentityHashMap;
import java.util.Map;

import wyal.heap.SyntacticHeaps;
import wyal.lang.Formula;
import wyal.lang.Proof;
import wyal.lang.SyntacticItem;
import wyal.lang.WyalFile;
import wyal.lang.Proof.State;
import wyal.lang.WyalFile.Declaration;
import wyal.lang.WyalFile.Expr;
import wyal.lang.WyalFile.Tuple;
import wyal.lang.WyalFile.Type;
import wyal.lang.WyalFile.VariableDeclaration;
import wyal.lang.WyalFile.Stmt.Block;
import wyal.util.Formulae;
import wyal.util.TypeSystem;

/**
 * <p>
 * Responsible for inlining macro invocations from their definitions. For
 * example, consider this assertion:
 * </p>
 *
 * <pre>
 * define nat(int n) is:
 *   n >= 0
 *
 * assert:
 *   forall(int x):
 *       if:
 *           x > 0
 *       then:
 *           nat(x)
 * </pre>
 * <p>
 * In proving this assertion, we will at some point come to the macro invocation
 * <code>nat(x)</code> or its <i>inversion</i> <code>!nat(x)</code>. To deal
 * with this, we simply replace <code>nat(x)</code> by its body where the
 * parameters are substituted for their arguments. That is, we replace
 * <code>nat(x)</code> by <code>n >= 0</code> and substitute <code>n</code> for
 * the argument <code>x</code>.
 * </p>
 * <p>
 * <b>NOTE:</b> A pretty obvious concern with this rule is how to deal with
 * recursive macro definitions. This has not been tried and tested at this
 * stage!
 * </p>
 *
 * @author <NAME>
 *
 */
public class MacroExpansion implements Proof.LinearRule {
	private final TypeSystem types;

	public MacroExpansion(TypeSystem types) {
		this.types = types;
	}

	@Override
	public String getName() {
		return "Macro-I";
	}

	@Override
	public State apply(Proof.State state, Formula truth) {
		Formula expanded = expandFormula(truth);
		if(expanded != truth) {
			expanded = state.allocate(expanded);
			state = state.subsume(this, truth, expanded);
		}
		return state;
	}

	private Formula expandFormula(Formula formula) {
		if (formula instanceof Formula.Invoke) {
			Formula.Invoke ivk = (Formula.Invoke) formula;
			// Determine the type declaration in question
			Type.FunctionOrMacro af = ivk.getSignatureType();
			// Resolve the declaration corresponding to this invocation
			Declaration.Named decl = types.resolveAsDeclaration(ivk.getName());
			// Calculate the invariant (if any)
			Formula invariant = extractDeclarationInvariant(decl, ivk.getArguments());
			if (invariant != null) {
				if (!ivk.getSign()) {
					invariant = Formulae.invert(invariant);
				}
				// Update the state
				return Formulae.simplifyFormula(invariant,types);
			}
		} else if(formula instanceof Formula.Quantifier) {
			Formula.Quantifier quantifier = (Formula.Quantifier) formula;
			if(quantifier.getSign()) {
				// There's no point going into existentials since they will be
				// expanded anyway,
				Formula body = expandFormula(quantifier.getBody());
				if(body != quantifier.getBody()) {
					quantifier = new Formula.Quantifier(true, quantifier.getParameters(), body);
					return Formulae.simplifyFormula(quantifier, types);
				}
			}
		} else if(formula instanceof Formula.Disjunct) {
			Formula.Disjunct disjunct = (Formula.Disjunct) formula;
			Formula[] children = disjunct.getOperands();
			Formula[] nChildren = expandFormula(children);
			if(nChildren != children) {
				disjunct = new Formula.Disjunct(nChildren);
				return Formulae.simplifyFormula(disjunct, types);
			}
		} else if(formula instanceof Formula.Conjunct) {
			Formula.Conjunct disjunct = (Formula.Conjunct) formula;
			Formula[] children = disjunct.getOperands();
			Formula[] nChildren = expandFormula(children);
			if(nChildren != children) {
				disjunct = new Formula.Conjunct(nChildren);
				return Formulae.simplifyFormula(disjunct, types);
			}
		}
		return formula;
	}

	private Formula[] expandFormula(Formula... children) {
		Formula[] nChildren = children;
		for(int i=0;i!=children.length;++i) {
			Formula child = nChildren[i];
			Formula nChild = expandFormula(child);
			if(child != nChild && nChildren == children) {
				nChildren = Arrays.copyOf(children, children.length);
			}
			nChildren[i] = nChild;
		}
		return nChildren;
	}

	private Formula extractDeclarationInvariant(Declaration.Named decl, Tuple<Expr> arguments) {
		if (decl instanceof Declaration.Named.Type) {
			// This is a type invariant macro call. In such case, we
			// need to first determine what the invariant actually is.
			Declaration.Named.Type td = (Declaration.Named.Type) decl;
			// Expand the corresponding type invariant
			return expandTypeInvariant(td, arguments.getOperand(0));
		} else if (decl instanceof Declaration.Named.Macro) {
			Declaration.Named.Macro md = (Declaration.Named.Macro) decl;
			// Expand the macro body with appropriate substitutions
			return expandMacroBody(md, arguments.getOperands());
		} else {
			// Functions are ignored
			return null;
		}
{'fraction_non_alphanumeric': 0.1150422014105677, 'fraction_numerical': 0.001040582726326743, 'mean_word_length': 3.84593837535014, 'pattern_counts': {'":': 0, '<': 59, '<?xml version=': 0, '>': 65, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2484583', 'n_tokens_mistral': 2965, 'n_tokens_neox': 2673, 'n_words': 766}