pga/congruence.ml

open Types

let rec unfold_repeat = function
  | Repeat (_, 0) as i :: _ ->
    raise (Ins_error (i, "cannot repeat 0 times"))
  | Repeat (i, 1) :: tl ->
    i :: unfold_repeat tl
  | Repeat (i, n) :: tl ->
    i :: unfold_repeat (Repeat (i, n - 1) :: tl)
  | hd :: tl ->
    hd :: unfold_repeat tl
  | [] -> []

let rec norm = function
  | [] -> N 0
  | Repeat (i, t) :: tl -> norm [i] ** (N t) ++ norm tl
  | Loop _ :: tl -> Infinity
  | Concat l :: tl -> norm l ++ norm tl
  | hd :: tl -> N 1 ++ norm tl