<commit_before>functor LevelSolver (Syntax : SYNTAX_WITH_UNIVERSES) :>
  LEVEL_SOLVER
    where type term = Syntax.t
    where type Level.t = Syntax.Level.t =
struct
  open Syntax

  infix $ \
  type term = Syntax.t

  exception LevelSolver

  local
    structure Dict = SplayDict(structure Key = Variable)
    open Dict

    fun go H (` x, ` y) R =
          let
            open Variable
          in
            if eq (x, y) orelse eq (lookup H x, y) orelse eq (lookup H y, x) then
              R
            else
              raise LevelSolver
          end
      | go H (x \ E, y \ F) R = go (insert H x y) (out E, out F) R
      | go H (O1 $ ES1, O2 $ ES2) R =
          (case (getLevelParameter O1, getLevelParameter O2) of
                (SOME k, SOME l) => goes H (ES1, ES2) (Level.unify (k,l) :: R)
              | (NONE, NONE) =>
                  if Operator.eq (O1, O2) then
                    goes H (ES1, ES2) R
                  else
                    raise LevelSolver
              | _ => raise LevelSolver)
      | go _ _ _ = raise LevelSolver
    and goes H (xs, ys) R =
          let
            val length = Vector.length xs
            val _ = if Vector.length ys <> length then raise LevelSolver else ()
            val xsys = Vector.tabulate (length, fn n => (Vector.sub (xs, n), Vector.sub (ys, n)))
          in
            Vector.foldl (fn ((M,N), R') => go H (out M, out N) R') R xsys
          end
  in
    fun generateConstraints (M, N) = go empty (out M, out N) []
  end

  fun subst f M =
    case out M of
         ` x => into (` x)
       | O $ ES => into (mapLevel f O $ Vector.map (subst f) ES)
       | x \ E => into (x \ subst f E)
end

functor SyntaxWithUniverses
  (type label
   structure Syntax : ABT
     where type Operator.t = label OperatorType.operator
  ) : SYNTAX_WITH_UNIVERSES =
struct
  open Syntax
  structure Level = Level<commit_msg>Ensure that LevelSolver always checks that operators are equal<commit_after>functor LevelSolver (Syntax : SYNTAX_WITH_UNIVERSES) :>
  LEVEL_SOLVER
    where type term = Syntax.t
    where type Level.t = Syntax.Level.t =
struct
  open Syntax

  infix $ \
  type term = Syntax.t

  exception LevelSolver

  local
    structure Dict = SplayDict(structure Key = Variable)
    open Dict

    fun go H (` x, ` y) R =
          let
            open Variable
          in
            if eq (x, y) orelse eq (lookup H x, y) orelse eq (lookup H y, x) then
              R
            else
              raise LevelSolver
          end
      | go H (x \ E, y \ F) R = go (insert H x y) (out E, out F) R
      | go H (O1 $ ES1, O2 $ ES2) R =
        if Operator.eq (O1, O2) then
            case (getLevelParameter O1, getLevelParameter O2) of
                (SOME k, SOME l) => goes H (ES1, ES2) (Level.unify (k,l) :: R)
              | (NONE, NONE) => goes H (ES1, ES2) R
              | _ => raise LevelSolver
        else
            raise LevelSolver
      | go _ _ _ = raise LevelSolver
    and goes H (xs, ys) R =
          let
            val length = Vector.length xs
            val _ = if Vector.length ys <> length then raise LevelSolver else ()
            val xsys = Vector.tabulate (length, fn n => (Vector.sub (xs, n), Vector.sub (ys, n)))
          in
            Vector.foldl (fn ((M,N), R') => go H (out M, out N) R') R xsys
          end
  in
    fun generateConstraints (M, N) = go empty (out M, out N) []
  end

  fun subst f M =
    case out M of
         ` x => into (` x)
       | O $ ES => into (mapLevel f O $ Vector.map (subst f) ES)
       | x \ E => into (x \ subst f E)
end

functor SyntaxWithUniverses
  (type label
   structure Syntax : ABT
     where type Operator.t = label OperatorType.operator
  ) : SYNTAX_WITH_UNIVERSES =
struct
  open Syntax
  structure Level = Level
{'fraction_non_alphanumeric': 0.0965444473753627, 'fraction_numerical': 0.006330783434450013, 'mean_word_length': 1.676076217360621, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 23, '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': '2945872', 'n_tokens_mistral': 1288, 'n_tokens_neox': 1247, 'n_words': 467}