kbc.cs

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;

namespace TRS
{
    class VF
    {
        public VF()
        { }
    }

    class V : VF
    {
        public V(string str)
        {
            this.str = str;
        }

        string str;
    }

    class F : VF
    {
        public F(string str)
        {
            this.str = str;
        }
        
        string str;
    }

    class Term
    {
        public Term(bool isVar, VF root, List<Term> args)
        {
            this.isVar = isVar;
            this.root = root;
            this.args = args;
        }

        public SortedSet<F> Funs()
        {
            return AddFuns(new SortedSet<F>());
        }

        public SortedSet<Util.Pair<F, int>> FunsAris()
        {
            return AddFunAris(new SortedSet<Util.Pair<F, int>>());
        }

        public virtual SortedSet<V> AddVars(SortedSet<V> xs)
        {
            return null;
        }

        public virtual SortedSet<F> AddFuns(SortedSet<F> fs)
        {
            return null;
        }

        public virtual SortedSet<Util.Pair<F, int>> AddFunAris(SortedSet<Util.Pair<F, int>> fs)
        {
            return null;
        }

        public int Size()
        {
            if (isVar)
            {
                return 1;
            }
            else
            {
                int r = 1;
                foreach (Term t in args)
                {
                    r += t.Size();
                }
                return r;
            }
        }

        public int Depth()
        {
            if (isVar || args.Count() == 0)
            {
                return 0;
            }
            else
            {
                int r = 0;
                foreach (Term t in args)
                {
                    r = Math.Max(t.Depth(), r);
                }
                return r + 1;
            }
        }

        public bool SubTerm(Term that)
        {
            if (that.isVar)
            {
                return false;
            }
            else
            {
                foreach (Term t in args)
                {
                    return t == that || t.SubTerm(that);
                }
            }
            return false;
        }

        public virtual SortedSet<Term> AddSubTerm(SortedSet<Term> ss)
        {
            return null;
        }

        public bool isVar;
        public VF root;
        public List<Term> args;
    }

    class Var : Term
    {
        public Var(string name) : base(true, new V(name), null)
        { }

        public override SortedSet<V> AddVars(SortedSet<V> xs)
        {
            xs.Add((V)root);
            return xs;
        }

        public override SortedSet<F> AddFuns(SortedSet<F> fs)
        {
            return fs;
        }

        public override SortedSet<Util.Pair<F, int>> AddFunAris(SortedSet<Util.Pair<F, int>> fs)
        {
            return fs;
        }

        public override SortedSet<Term> AddSubTerm(SortedSet<Term> ss)
        {
            ss.Add(this);
            return ss;
        }
    }

    class Fun : Term
    {
        public Fun(string name, List<Term> args) : base(false, new F(name), args)
        { }

        public override SortedSet<V> AddVars(SortedSet<V> xs)
        {
            return Util.FoldLeft(args, xs, (s, t) => t.AddVars(s));
        }

        public override SortedSet<F> AddFuns(SortedSet<F> fs)
        {
            fs.Add((F)root);
            return Util.FoldLeft(args, fs, (s, t) => t.AddFuns(s));
        }

        public override SortedSet<Util.Pair<F, int>> AddFunAris(SortedSet<Util.Pair<F, int>> fs)
        {
            fs.Add(new Util.Pair<F, int>((F)root, args.Count()));
            return Util.FoldLeft(args, fs, (s, t) => t.AddFunAris(s));
        }

        public override SortedSet<Term> AddSubTerm(SortedSet<Term> ss)
        {
            ss.Add(this);
            return Util.FoldLeft(args, ss, (s, t) => t.AddSubTerm(s));
        }
    }

    class UnifyException : Exception
    { }

    class NormException : Exception
    { }

    class CompletionFailedException : Exception
    { }

    static class Util
    {
        public class Pair<T1, T2>
        {
            public Pair(T1 first, T2 second)
            {
                this.first = first;
                this.second = second;
            }

            public T1 first;
            public T2 second;
        }

        public static T FoldLeft<T, U>(this IEnumerable<U> source, T acc, Func<T, U, T> func)
        {
            for (int index = 0; index < source.Count<U>(); index++)
                acc = func(acc, source.ElementAt(index));
            return acc;
        }
    }

    class Program
    {
        static void Main(string[] args)
        {
        }
    }
}