<commit_before>package org.ai4fm.proofprocess.isabelle.core.parse;

import isabelle.Markup;
import isabelle.Pretty;
import isabelle.XML.Elem;
import isabelle.XML.Text;
import isabelle.XML.Tree;
import isabelle.scala.ScalaCollections;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.Stack;

import org.ai4fm.proofprocess.Term;
import org.ai4fm.proofprocess.isabelle.CompositeTerm;
import org.ai4fm.proofprocess.isabelle.DisplayTerm;
import org.ai4fm.proofprocess.isabelle.IsaTerm;
import org.ai4fm.proofprocess.isabelle.IsabelleProofProcessFactory;
import org.ai4fm.proofprocess.isabelle.TermKind;

import scala.Tuple2;
import scala.collection.Iterator;

/**
 * @author <NAME>
 */
public class TermParser {

	private static IsabelleProofProcessFactory FACTORY = IsabelleProofProcessFactory.eINSTANCE;
	
	private static Set<String> IGNORE_MARKUPS = Collections.unmodifiableSet(new HashSet<String>(Arrays.asList(
			Markup.BREAK())));
	
	public static List<Term> parseGoals(Tree source) {
		
		List<Term> goals = new ArrayList<Term>();
		
		// get all XML elements for <subgoal>
		for (Elem subgoalElem : getElems(ScalaCollections.singletonList(source), Markup.SUBGOAL())) {
			// expect a single <term> XML element inside
			Elem termElem = getSingleElem(subgoalElem.body(), Markup.TERM());
			Term ppTerm = parseTerm(termElem);
			goals.add(ppTerm);
		}
		
		return goals;
	}
	
	private static List<Elem> getElems(scala.collection.immutable.List<Tree> source, String markup) {
		List<Elem> elems = new ArrayList<Elem>();
		collectElems(source, markup, elems);
		return elems;
	}
	
	private static void collectElems(scala.collection.immutable.List<Tree> source, String markup,
			List<Elem> elems) {
		for (Iterator<Tree> it = source.iterator(); it.hasNext();) {
			Tree obj = it.next();
			if (obj instanceof Elem) {
				Elem elem = (Elem) obj;

				if (markup.equals(elem.markup().name())) {
					// found elem with correct markup
					elems.add(elem);
				} else {
					// recurse deeper
					collectElems(elem.body(), markup, elems);
				}
			}
		}
	}
	
	private static Elem getSingleElem(scala.collection.immutable.List<Tree> body, String markup) {
		List<Elem> elems = getElems(body, markup);
		if (elems.size() == 1) {
			// if single element found, return it
			return elems.get(0);
		}
		
		// invalid cases
		if (elems.isEmpty()) {
			throw new IllegalArgumentException("No <" + markup + "> found: " + body);
		}
		
		throw new IllegalArgumentException("Multiple <" + markup + "> found: " + body);
	}
	
	private static Term parseTerm(Elem termElem) {
		// do the parsing - ensuring its TERM
		if (!Markup.TERM().equals(termElem.markup().name())) {
			throw new IllegalArgumentException("Expected <term>, found: " + termElem);
		}
		
		CompositeTermParser parser = new CompositeTermParser();
		parser.parse(termElem.body());
		
		Term term = parser.rootTerm;
		if (term == null) {
			throw new IllegalStateException("Invalid term: " + termElem);
		}
		
		return term;
	}
	
	private static class CompositeTermParser {
		
		private final Stack<DisplayTerm> termStack = new Stack<DisplayTerm>();
		private Term rootTerm;
		
		public void parse(scala.collection.immutable.List<Tree> source) {
			
			for (Iterator<Tree> it = source.iterator(); it.hasNext();) {
				Tree e = it.next();
				
				if (e instanceof Text) {
					
					String content = ((Text) e).content();
					
					DisplayTerm top = termStack.peek();
					if (top instanceof IsaTerm) {
						IsaTerm isaTerm = (IsaTerm) top;
						if (isaTerm.getName() == null) {
							isaTerm.setName(content);
						} else {
							// usually happens for CONST entities, they have a fully-qualified name
							// and a "display" text inside
//							System.out.println("Term name already set. Text: " + content + ";\nTerm: " + isaTerm);
						}
					} else {
						// usually happens for CompositeTerms, when parentheses are used, 
						// e.g. composite would have ["(", IsaTerm, ")"]. 
//						System.out.println("Text element inside a non-term. Text: " + content + ";\nTerm: " + top);
					}
					
				} else if (e instanceof Elem) {
					Elem elem = (Elem) e;
					Markup markup = elem.markup();
					
					if (Markup.BLOCK().equals(markup.name()) && getElemCount(elem.body()) == 1) {
			            // single element inside a block - continue on the inner element,
			            // skipping the outer BLOCK. 
						// Note that we ignore the inner Texts in this check.
						parse(elem.body());
					} else if (ignoreElem(markup.name())){
						// Some elements are in result XML for pretty-printing
						// only, and should be ignored in parsing altogether, e.g. <break>.
						// Do nothing for this elem - continue onto the next one
						continue;
					} else {
						<commit_msg>Text-only blocks are also skipped<commit_after>package org.ai4fm.proofprocess.isabelle.core.parse;

import isabelle.Markup;
import isabelle.Pretty;
import isabelle.XML.Elem;
import isabelle.XML.Text;
import isabelle.XML.Tree;
import isabelle.scala.ScalaCollections;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.Stack;

import org.ai4fm.proofprocess.Term;
import org.ai4fm.proofprocess.isabelle.CompositeTerm;
import org.ai4fm.proofprocess.isabelle.DisplayTerm;
import org.ai4fm.proofprocess.isabelle.IsaTerm;
import org.ai4fm.proofprocess.isabelle.IsabelleProofProcessFactory;
import org.ai4fm.proofprocess.isabelle.TermKind;

import scala.Tuple2;
import scala.collection.Iterator;

/**
 * @author <NAME>
 */
public class TermParser {

	private static IsabelleProofProcessFactory FACTORY = IsabelleProofProcessFactory.eINSTANCE;
	
	private static Set<String> IGNORE_MARKUPS = Collections.unmodifiableSet(new HashSet<String>(Arrays.asList(
			Markup.BREAK())));
	
	public static List<Term> parseGoals(Tree source) {
		
		List<Term> goals = new ArrayList<Term>();
		
		// get all XML elements for <subgoal>
		for (Elem subgoalElem : getElems(ScalaCollections.singletonList(source), Markup.SUBGOAL())) {
			// expect a single <term> XML element inside
			Elem termElem = getSingleElem(subgoalElem.body(), Markup.TERM());
			Term ppTerm = parseTerm(termElem);
			goals.add(ppTerm);
		}
		
		return goals;
	}
	
	private static List<Elem> getElems(scala.collection.immutable.List<Tree> source, String markup) {
		List<Elem> elems = new ArrayList<Elem>();
		collectElems(source, markup, elems);
		return elems;
	}
	
	private static void collectElems(scala.collection.immutable.List<Tree> source, String markup,
			List<Elem> elems) {
		for (Iterator<Tree> it = source.iterator(); it.hasNext();) {
			Tree obj = it.next();
			if (obj instanceof Elem) {
				Elem elem = (Elem) obj;

				if (markup.equals(elem.markup().name())) {
					// found elem with correct markup
					elems.add(elem);
				} else {
					// recurse deeper
					collectElems(elem.body(), markup, elems);
				}
			}
		}
	}
	
	private static Elem getSingleElem(scala.collection.immutable.List<Tree> body, String markup) {
		List<Elem> elems = getElems(body, markup);
		if (elems.size() == 1) {
			// if single element found, return it
			return elems.get(0);
		}
		
		// invalid cases
		if (elems.isEmpty()) {
			throw new IllegalArgumentException("No <" + markup + "> found: " + body);
		}
		
		throw new IllegalArgumentException("Multiple <" + markup + "> found: " + body);
	}
	
	private static Term parseTerm(Elem termElem) {
		// do the parsing - ensuring its TERM
		if (!Markup.TERM().equals(termElem.markup().name())) {
			throw new IllegalArgumentException("Expected <term>, found: " + termElem);
		}
		
		CompositeTermParser parser = new CompositeTermParser();
		parser.parse(termElem.body());
		
		Term term = parser.rootTerm;
		if (term == null) {
			throw new IllegalStateException("Invalid term: " + termElem);
		}
		
		return term;
	}
	
	private static class CompositeTermParser {
		
		private final Stack<DisplayTerm> termStack = new Stack<DisplayTerm>();
		private Term rootTerm;
		
		public void parse(scala.collection.immutable.List<Tree> source) {
			
			for (Iterator<Tree> it = source.iterator(); it.hasNext();) {
				Tree e = it.next();
				
				if (e instanceof Text) {
					
					String content = ((Text) e).content();
					
					DisplayTerm top = termStack.peek();
					if (top instanceof IsaTerm) {
						IsaTerm isaTerm = (IsaTerm) top;
						if (isaTerm.getName() == null) {
							isaTerm.setName(content);
						} else {
							// usually happens for CONST entities, they have a fully-qualified name
							// and a "display" text inside
//							System.out.println("Term name already set. Text: " + content + ";\nTerm: " + isaTerm);
						}
					} else {
						// usually happens for CompositeTerms, when parentheses are used, 
						// e.g. composite would have ["(", IsaTerm, ")"]. 
//						System.out.println("Text element inside a non-term. Text: " + content + ";\nTerm: " + top);
					}
					
				} else if (e instanceof Elem) {
					Elem elem = (Elem) e;
					Markup markup = elem.markup();
					
					if (Markup.BLOCK().equals(markup.name()) && getElemCount(elem.body()) <= 1) {
			            // single element inside a block - continue on the inner element,
			            // skipping the outer BLOCK. 
						// Note that we ignore the inner Texts in this check.
						parse(elem.body());
					} else if (ignoreElem(markup.name())){
						// Some elements are in result XML for pretty-printing
						// only, and should be ignored in parsing altogether, e.g. <break>.
						// Do nothing for this elem - continue onto the next one
						continue;
					} else {
						
{'fraction_non_alphanumeric': 0.1262677484787018, 'fraction_numerical': 0.002231237322515213, 'mean_word_length': 3.298605056669573, 'pattern_counts': {'":': 0, '<': 54, '<?xml version=': 0, '>': 53, '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': '3408587', 'n_tokens_mistral': 3720, 'n_tokens_neox': 3037, 'n_words': 806}