core.ml

module L = List
open Set
open Util
open Log

(** Simple types  *)
type simple_type =
  | O  (** the base type O *)
  | Imp of simple_type * simple_type
  | UnT  (** untyped *)

(** Syntactic sugar  *)
let imp a b = Imp (a, b)

(** Calculates the order of a type. *)
let rec ord = function
  | UnT -> -1
  | O -> 0
  | Imp (s, t) -> max (ord s + 1) (ord t)

(** Checks if a type is homogeneous.
  A type is said to be homogeneous if for each implication,
  the order of the type on the left hand side is greater equal
  the order of the type on the right hand side.
*)
let rec homogeneous = function
  | O -> true
  | Imp (s, t) -> ord s >= ord t && homogeneous s && homogeneous t
  | UnT -> true

(** Retuns a typ as string *)
let rec typ_to_string = function
  | O -> "o"
  | Imp (l, r) -> "(" ^ typ_to_string l ^ "→" ^ typ_to_string r ^ ")"
  | UnT -> "UnT"

(** Type definition of the a term.
  Each abstraction, application and variable has additional information
  about the type and the position in the term.
*)
type a_term =
  | AVar of string * simple_type
  | ALam of ((string * simple_type) * a_term) * simple_type
  | AApp of a_term * a_term * simple_type

(* | Beta of (string * simple_type) * a_term * a_term *)

(** Returns a list of pairs of type string * typ as string *)
let rec ctx_to_string = function
  | [] -> ""
  | [ x ] -> fst x ^ ":" ^ typ_to_string (snd x)
  | x :: xs -> fst x ^ ":" ^ typ_to_string (snd x) ^ ", " ^ ctx_to_string xs

let rec _a_term_to_string term =
  match term with
  | AVar (s, _) -> s
  | ALam (((s, vt), t), tp) -> (
      match vt with
      | UnT -> "λ" ^ s ^ "." ^ _a_term_to_string t
      | _ -> "λ" ^ s ^ "^" ^ typ_to_string vt ^ "." ^ _a_term_to_string t )
  | AApp (x, y, tp) -> (
      match (x, y) with
      | AVar _, AVar _ -> _a_term_to_string x ^ " " ^ _a_term_to_string y
      | AVar _, _ -> _a_term_to_string x ^ " (" ^ _a_term_to_string y ^ ")"
      | _, AVar _ -> "(" ^ _a_term_to_string x ^ ") " ^ _a_term_to_string y
      | _, _ -> "(" ^ _a_term_to_string x ^ ") (" ^ _a_term_to_string y ^ ")" )

(** Convert a {e a_term} to string  *)
let a_term_to_string term = _a_term_to_string term

(* let rec _a_term_to_string2 term =
  match term with
  | AVar (s, _) -> s
  | ALam (((s, vt), t), tp) ->
      (String.make 1 '\\') ^ s ^ " -> " ^ _a_term_to_string2 t
  | AApp (x, y, tp) -> (
      match (x, y) with
      | AVar _, AVar _ -> _a_term_to_string2 x ^ " " ^ _a_term_to_string2 y
      | AVar _, _ -> _a_term_to_string2 x ^ " (" ^ _a_term_to_string2 y ^ ")"
      | _, AVar _ -> "(" ^ _a_term_to_string2 x ^ ") " ^ _a_term_to_string2 y
      | _, _ -> "(" ^ _a_term_to_string2 x ^ ") (" ^ _a_term_to_string2 y ^ ")" )

(** Convert a {e a_term} to string  *)
let a_term_to_string2 term = _a_term_to_string2 term *)

(** Extract the name of a variable from a {e a_term}  *)
let vname = function AVar (n, _) -> n | _ -> ""

(** Extract the type from a {e a_term}  *)
let ttyp = function
  | AVar (_, typ) -> typ
  | ALam (_, typ) -> typ
  | AApp (_, _, typ) -> typ

let rec _assignments tterm =
  match tterm with
  | AVar (v, t) -> [ (v, t) ]
  | ALam ((xs, t), _) -> xs :: _assignments t
  | AApp (x, y, t) -> _assignments x @ _assignments y

(** Extract all the type assignments in a term attached to a given context  *)
let assignments ctx tterm = ctx @ _assignments tterm

let rec _order_consistent ass =
  match ass with
  | [] -> true
  | x :: xs ->
      let fl =
        List.find_all (fun y -> fst y = fst x && ord (snd y) != ord (snd x)) xs
      in
      if fl = [] then _order_consistent xs else false

(** Checks if a term satisfies the safe typing convention (order consistent).
    The type assignments in a term are said to be order consistent,
    if all the types assigned to a variable are of the same order *)
let order_consistent tterm = _order_consistent (_assignments tterm)

(** Extract the free variables in a {e a_term}  *)
let rec free_variables = function
  | AVar (x, t) -> [ AVar (x, t) ]
  | ALam ((x, e), t) -> remove (free_variables e) vname (fst x)
  | AApp (x, y, t) -> free_variables x @ free_variables y

(** Extract the free variables in a list of {e a_term}s  *)
let rec free_variables_list = function
  | [] -> []
  | x :: xs -> free_variables x @ free_variables_list xs

let rec binders = function
  | AVar (x, t) -> []
  | ALam ((x, e), t) -> x :: binders e
  | AApp (x, y, t) -> binders x @ binders y

let rec _safe_naming = function
  | [] -> true
  | x :: xs -> (not (List.exists (( = ) x) xs)) && _safe_naming xs

let safe_naming tterm =
  let fvs = L.map vname (free_variables tterm) in
  let binders = L.map fst (binders tterm) in
  let vars = fvs @ binders in
  _safe_naming vars

let rec _make_closed fvs term =
  match fvs with
  | [] -> term
  | x :: xs -> _make_closed xs (ALam ((x, term), UnT))

let make_closed term =
  let fvs = free_variables term in
  _make_closed
    (L.map
       (fun x ->
         match x with
         | AVar (x, t) -> (x, t)
         | _ -> failwith "Not var type tuple")
       fvs)
    term

let rec issafe tterm =
  let fvs = free_variables tterm in
  let minord = L.fold_left min 100 (L.map ord (L.map ttyp fvs)) in
  (* Printf.printf "%d %s:%d\n" minord (a_term_to_string tterm) (ord (ttyp tterm)); *)
  match tterm with
  | AVar _ -> true
  | AApp (x, y, typ) -> issafe x && issafe y
  | ALam ((vs, st), typ) -> (
      minord >= ord typ
      && match st with AApp (x, y, _) -> issafe x && issafe y | _ -> issafe st )

(** Symbols as used in the AST. *)
type symbol = VS of string | LS of (string * simple_type) | AS of string

let rec term_nodes_r tterm pos =
  match tterm with
  | AVar (s, typ) -> [ (pos, VS s, typ) ]
  | ALam ((xs, t), typ) -> (pos, LS xs, typ) :: term_nodes_r t (pos ^ "0")
  | AApp (x, y, typ) ->
      let app_node = (pos, AS "@", typ) in
      app_node :: (term_nodes_r x (pos ^ "0") @ term_nodes_r y (pos ^ "1"))

let term_nodes tterm = term_nodes_r tterm "e"

(** Extract the free variables in a {e a_term}  *)
let rec _free_variables_pos tterm pos =
  match tterm with
  | AVar (x, t) -> [ (pos, x) ]
  | ALam ((x, y), t) -> remove (_free_variables_pos y (pos ^ "0")) snd (fst x)
  | AApp (x, y, t) ->
      _free_variables_pos x (pos ^ "0") @ _free_variables_pos y (pos ^ "1")

let free_variables_pos tterm = _free_variables_pos tterm "e"

let rec gentuples pos fvs =
  match fvs with [] -> [] | x :: xs -> [ x; pos ] :: gentuples pos xs

let rec b_edges_r tterm pos =
  match tterm with
  | AVar _ -> []
  | ALam ((xs, t), _) ->
      let fvs = _free_variables_pos t (pos ^ "0") in
      let vs = fst xs in
      let bfvs =
        L.map fst (L.filter (fun (p, x) -> if x = vs then true else false) fvs)
      in
      let bpairs = gentuples pos bfvs in
      bpairs @ b_edges_r t (pos ^ "0")
  | AApp (x, y, typ) -> b_edges_r x (pos ^ "0") @ b_edges_r y (pos ^ "1")

let b_edges tterm = b_edges_r tterm "e"

let rec c_edges_r tterm pos =
  match tterm with
  | AVar _ -> []
  | ALam ((xs, t), _) ->
      let fvs = _free_variables_pos t (pos ^ "0") in
      let vs = fst xs in
      let cfvs =
        L.map fst (L.filter (fun (p, x) -> if x = vs then false else true) fvs)
      in
      let cpairs = gentuples pos cfvs in
      cpairs @ c_edges_r t (pos ^ "0")
  | AApp (x, y, typ) -> c_edges_r x (pos ^ "0") @ c_edges_r y (pos ^ "1")

let c_edges tterm = c_edges_r tterm "e"

let rec a_edges_r tterm pos =
  match tterm with
  | AVar _ -> []
  | ALam ((xs, t), _) -> a_edges_r t (pos ^ "0")
  | AApp (x, y, typ) ->
      let fvs = L.map fst (_free_variables_pos y (pos ^ "1")) in
      let pairs = gentuples pos fvs in
      pairs @ a_edges_r x (pos ^ "0") @ a_edges_r y (pos ^ "1")

let a_edges tterm = a_edges_r tterm "e"

let get_node pos nodes = L.filter (fun (p, _, _) -> p = pos) nodes

(** first n elements of list *)
let rec cutlist l n =
  match (l, n) with
  | [], _ -> []
  | _, 0 -> []
  | x :: xs, _ -> x :: cutlist xs (n - 1)

let node_tostring = function
  | p, AS s, _ -> p ^ "-@"
  | p, LS vs, _ -> p ^ "-λ" ^ fst vs
  | p, VS s, _ -> p ^ "-" ^ s

type wbp = Empty | Node of string * symbol * simple_type | Comp of wbp list

let posymtyp_to_node = function p, s, t -> Node (p, s, t)

let append_wbp p n =
  match p with
  | Empty -> n
  | Node _ -> Comp [ p; n ]
  | Comp xs -> Comp (xs @ [ n ])

(* | Comp xs -> Comp ([p; n]) *)

let rec wbp_tolist = function
  | Empty -> []
  | Node (pos, sym, typ) -> [ pos ]
  | Comp [] -> []
  | Comp (x :: xs) -> wbp_tolist x @ wbp_tolist (Comp xs)

let rec wbp_tosymlevellist level = function
  | Empty -> []
  | Node (pos, sym, typ) -> [ (pos, sym, level) ]
  | Comp [] -> []
  | Comp (x :: xs) ->
      wbp_tosymlevellist (level + 1) x @ wbp_tosymlevellist level (Comp xs)

let wbp_tosymlevellist wbp = wbp_tosymlevellist 0 wbp

let rec wbp_tosymlist = function
  | Empty -> []
  | Node (pos, sym, typ) -> [ (pos, sym) ]
  | Comp [] -> []
  | Comp (x :: xs) -> wbp_tosymlist x @ wbp_tosymlist (Comp xs)

let sym_tostring = function AS s -> "@" | LS vs -> "λ" ^ fst vs | VS s -> s

let isapp = function AS _ -> true | _ -> false

let rec _wbp_tostring path flag =
  match (path, flag) with
  | Empty, _ -> ""
  | Node (pos, sym, typ), _ -> sym_tostring sym ^ "-" ^ pos
  | Comp _, false -> "[" ^ _wbp_tostring path true ^ "]"
  | Comp [], _ -> ""
  | Comp [ x ], _ -> _wbp_tostring x false
  | Comp (x :: xs), _ ->
      _wbp_tostring x false ^ ", " ^ _wbp_tostring (Comp xs) true

let wbp_tostring path = _wbp_tostring path false

let rec _reverse_wbp p flag =
  match (p, flag) with
  | Empty, _ -> Empty
  | Node (pos, sym, typ), _ -> Node (pos, sym, typ)
  | Comp xs, false -> _reverse_wbp (Comp (L.rev xs)) true
  | Comp xs, _ -> Comp (L.map (fun x -> _reverse_wbp x false) xs)

let reverse_wbp p = _reverse_wbp p false

let rec wbp_tail p =
  match p with
  | Empty -> Empty
  | Node (pos, sym, typ) -> Empty
  | Comp (Node _ :: xs) -> Comp xs
  | Comp (x :: xs) -> append_wbp (wbp_tail x) (Comp xs)
  | Comp [] -> Empty

let rec last_wbp = function
  | Empty -> Empty
  | Node (pos, sym, typ) -> Node (pos, sym, typ)
  | Comp [ x ] -> last_wbp x
  | Comp (x :: xs) -> last_wbp (Comp xs)
  | _ -> failwith "Wbp wrong."

let rec first_wbp = function
  | Empty -> Empty
  | Node (pos, sym, typ) -> Node (pos, sym, typ)
  | Comp [ x ] -> first_wbp x
  | Comp (x :: _) -> first_wbp x
  | _ -> failwith "Wbp wrong."

let rec wbp_length = function
  | Empty -> 0
  | Node (pos, sym, typ) -> 1
  | Comp [] -> 0
  | Comp (x :: xs) -> wbp_length x + wbp_length (Comp xs)

let rec _wbp_sarting_at path i n =
  match path with
  | Comp (x :: xs) ->
      let len = wbp_length x in
      if i + len = n then path
      else if i + len < n then _wbp_sarting_at (Comp xs) (i + len) n
      else _wbp_sarting_at x i n
  | _ -> failwith "wbp_sarting_at not found."

let wbp_sarting_at path n = _wbp_sarting_at path 0 n

let rec wbp_ending_at path i =
  match path with
  | Comp (x :: xs) ->
      let len = wbp_length x in
      if len = i then x
      else if len < i then wbp_ending_at (Comp xs) (i - len)
      else wbp_ending_at x i
  | _ -> failwith "wbp_ending_at not found."

let decompose path s e =
  let path_l = wbp_tolist path in
  let w1 = wbp_ending_at path (s + 1) in
  let w1_l = wbp_tolist w1 in
  let w1_len = wbp_length w1 in
  let l1_idx = s - w1_len in
  let l1 = L.nth path_l l1_idx in
  let w2 = wbp_sarting_at path (e + 1) in
  let w2_l = wbp_tolist w2 in
  let w2_len = wbp_length w2 in
  let l2_idx = e + w2_len in
  let l2 = L.nth path_l l2_idx in
  let legal = l1 = l2 && w1_l = L.rev w2_l in
  legal

(* if not legal then (
  Printf.printf "\nl1 (%d): %s\n" l1_idx l1;
   Printf.printf "w1 (%d): %s\n" s (wbp_tostring w1);
   Printf.printf "cycle: %s\n" (list_tostring (sublist path_l s e) (fun x -> x));
   Printf.printf "w2 (%d): %s\n" e (wbp_tostring w2);
   Printf.printf "l2 (%d): %s\n\n" l2_idx l2;
   legal
 )
   else
     legal *)

let rec find_cycle path pa pb level s e idx =
  match path with
  | (px, _, lx) :: (py, sy, ly) :: xs ->
      if px = pa && py = pb then
        find_cycle ((py, sy, ly) :: xs) pa pb level s (e + 1) (idx + 1)
      else if px = pb && py = pa && level = lx && idx = 0 then [ (s, e + 1) ]
      else if px = pb && py = pa && level = lx && idx = 0 then
        find_cycle ((py, sy, ly) :: xs) pa pb level s (e + 1) (idx - 1)
      else find_cycle ((py, sy, ly) :: xs) pa pb level s (e + 1) idx
  | _ -> []

(* iterate over path, check if any cycle
  if no then legal
  otherwise check if call and return paths and discriminants are equal
 *)
let rec detect_cycles path idx =
  match path with
  | (pa, sa, _) :: (pb, sb, lb) :: xs ->
      let cxs = detect_cycles ((pb, sb, lb) :: xs) (idx + 1) in
      if isapp sa && pa ^ "1" = pb then
        let c = find_cycle ((pb, sb, lb) :: xs) pa pb lb idx (idx + 1) 0 in
        c @ cxs
      else cxs
  | _ -> []

let check_cycle path = function s, e -> decompose path s e

let is_legal = function
  | Empty -> false
  | path ->
      (* Printf.printf "Checking: %s\n" (wbp_tostring path); *)
      let cs = detect_cycles (wbp_tosymlevellist path) 0 in
      (* Printf.printf "Cycles found: %d\n" (L.length cs); *)
      let legal = L.fold_left ( && ) true (L.map (check_cycle path) cs) in
      (* Printf.printf "------------------------------------------------------------------------------------\n\n"; *)
      legal

let isvar_node = function Node (_, VS _, _) -> true | _ -> false

let islam_node = function Node (_, LS _, _) -> true | _ -> false

let isapp_node = function Node (_, AS _, _) -> true | _ -> false

let node_type = function
  | Node (_, x, _) -> x
  | _ -> failwith "node_type: not a node."

let node_pos = function
  | Node (p, _, _) -> p
  | _ -> failwith "node_pos: not a node."

let uniq_cons x xs = if L.mem x xs then xs else x :: xs

let linear_list xs = L.fold_right uniq_cons xs []

let rec lambda_composition_1 nodes varpath p_list =
  (* Printf.printf "\nlambda_composition_1: (%s)\n\n"  ((wbp_tostring) varpath); *)
  match p_list with
  | w :: ws ->
      let arg =
        posymtyp_to_node (L.hd (get_node (node_pos (first_wbp w) ^ "1") nodes))
      in
      (* Printf.printf "arg: (%s)\n"  (wbp_tostring arg);
         Printf.printf "append result: (%s)\n"  ((wbp_tostring) (append_wbp (append_wbp varpath (reverse_wbp w)) arg)); *)
      append_wbp (append_wbp varpath (reverse_wbp w)) arg
      :: lambda_composition_1 nodes varpath ws
  | [] -> [ Empty ]

let rec lambda_composition_2 nodes lampath p_list =
  (* Printf.printf "\nlambda_composition_2: (%s)\n\n"  ((wbp_tostring) lampath); *)
  match p_list with
  | w :: ws ->
      let arg =
        posymtyp_to_node
          (L.hd (get_node (node_pos (first_wbp lampath) ^ "1") nodes))
      in
      (* Printf.printf "arg: (%s)\n"  (wbp_tostring arg);
         Printf.printf "append result: (%s)\n"  ((wbp_tostring) (append_wbp (append_wbp w (reverse_wbp lampath)) arg)); *)
      append_wbp (append_wbp w (reverse_wbp lampath)) arg
      :: lambda_composition_2 nodes lampath ws
  | [] -> [ Empty ]

let rec app_composition nodes appapp applam_list =
  (* Printf.printf "\app_composition: (%s)\n\n"  ((wbp_tostring) p1); *)
  match applam_list with
  | y :: ys ->
      let body =
        posymtyp_to_node (L.hd (get_node (node_pos (last_wbp y) ^ "0") nodes))
      in
      let newpath = append_wbp (append_wbp appapp (wbp_tail y)) body in
      (* let newpath = append_wbp (append_wbp (reverse_wbp (wbp_tail (reverse_wbp appapp))) y) body in *)
      (* Printf.printf "APP_COMPOSITION\nAA: %s\nAL: %s\nRS: %s\n\n" (wbp_tostring appapp) (wbp_tostring y) (wbp_tostring newpath); *)
      newpath :: app_composition nodes appapp ys
  | [] -> [ Empty ]

let rec app_composition_2 nodes appapp_list applam =
  (* Printf.printf "\app_composition: (%s)\n\n"  ((wbp_tostring) p1); *)
  match appapp_list with
  | y :: ys ->
      let body =
        posymtyp_to_node
          (L.hd (get_node (node_pos (last_wbp applam) ^ "0") nodes))
      in
      let newpath = append_wbp (append_wbp y (wbp_tail applam)) body in
      (* Printf.printf "APP_COMPOSITION 2\nAA: %s\nAL: %s\nRS: %s\n\n" (wbp_tostring y) (wbp_tostring applam) (wbp_tostring newpath); *)
      newpath :: app_composition_2 nodes ys applam
  | [] -> [ Empty ]

let composition newpaths acc nodes bedges =
  let comp =
    L.map
      (fun x ->
        let lastnode = last_wbp x in
        match node_type lastnode with
        | VS _ -> (
            let bound = L.filter (fun y -> L.hd y = node_pos lastnode) bedges in
            match bound with
            | y :: _ ->
                let binder =
                  posymtyp_to_node (L.hd (get_node (llast y) nodes))
                in
                let wbps = L.filter (fun z -> last_wbp z = binder) newpaths in
                lambda_composition_1 nodes x wbps
            | [] -> [ Empty ] )
        | LS _ -> (
            (* get variables bound by lam node *)
            let vars =
              L.filter (fun y -> L.hd (L.rev y) = node_pos lastnode) bedges
            in
            let appapp = L.filter (fun x -> isapp_node (last_wbp x)) newpaths in
            let wbps = L.filter (fun y -> last_wbp y = first_wbp x) appapp in
            let app_comps = app_composition_2 nodes wbps x in
            match vars with
            | [] -> app_comps
            | _ ->
                let vars_pos = L.map (fun x -> L.hd x) vars in
                let wbps =
                  L.filter
                    (fun x -> L.mem (node_pos (last_wbp x)) vars_pos)
                    newpaths
                in
                app_comps @ lambda_composition_2 nodes x wbps )
        | AS _ ->
            let applam = L.filter (fun z -> islam_node (last_wbp z)) newpaths in
            let wbps = L.filter (fun y -> lastnode = first_wbp y) applam in
            (* wbps are the @-/x paths starting with an app other end with *)
            app_composition nodes x wbps)
      acc
  in
  L.filter is_legal (linear_list (L.flatten comp))

let rec similar_redex wbp = function
  | x :: xs ->
      first_wbp wbp = first_wbp x
      && last_wbp wbp = last_wbp x
      && islam_node (last_wbp x)
      || similar_redex wbp xs
  | [] -> false

let rec _well_balanced_paths newpaths acc nodes bedges n =
  (* Printf.printf "newpaths (%d)\n" (L.length newpaths);
     L.map (fun x -> Printf.printf "newpaths: (%s)\n" x) (L.map (wbp_tostring) newpaths); *)
  (* Printf.printf "newpaths (%d)\n" (L.length newpaths);
     Printf.printf "accpaths (%d)\n" (L.length acc); *)
  (* Printf.printf "---------------------------------------[%d]------------------------------------------\n\n" n; *)
  if n <= 0 then (false, acc)
  else
    let paths = composition newpaths acc nodes bedges in
    let newpaths =
      L.filter
        (fun x ->
          (not (L.mem x acc))
          && (not (first_wbp x = last_wbp x))
          && not (similar_redex x acc))
        paths
    in
    let newacc = acc @ newpaths in
    match newpaths with
    | [] -> (true, acc)
    | _ -> _well_balanced_paths newpaths newacc nodes bedges (n - 1)

let well_balanced_paths term =
  let nodes = term_nodes term in
  let bedges = b_edges term in
  let apps =
    L.filter (fun x -> match x with _, AS _, _ -> true | _ -> false) nodes
  in
  let acc =
    L.map
      (fun x ->
        match x with
        | pa, AS s, typ ->
            Comp
              [
                Node (pa, AS s, typ);
                posymtyp_to_node (L.hd (get_node (pa ^ "0") nodes));
              ]
        | _ -> Empty)
      apps
  in
  let max_compositions = 10 in
  let compose = _well_balanced_paths acc acc nodes bedges max_compositions in
  (* let applam = L.filter (fun p -> islam_node (last_wbp p)) (snd compose) in *)
  (fst compose, snd compose)

let well_balanced_paths_al term =
  let wbp = well_balanced_paths term in
  let applam = L.filter (fun p -> islam_node (last_wbp p)) (snd wbp) in
  (fst wbp, applam)

let legal_paths term =
  let wbp = well_balanced_paths_al term in
  (* let wbp = L.filter is_legal wbp in *)
  (fst wbp, L.map wbp_tolist (snd wbp))

let is_scc nodes path =
  let f = get_node (L.hd path) nodes in
  let l = get_node (L.hd (L.rev path)) nodes in
  match f with
  | (_, VS x, _) :: _ -> (
      match l with (_, LS vs, _) :: _ -> x = fst vs | _ -> false )
  | _ -> false

let arb_paths ae re be = melt_ll (melt_ll ae re) (L.map L.rev be)

let rec _scc arb cc stack i max_depth =
  if i > max_depth then (false, stack)
  else
    match cc with
    | [] -> (true, stack)
    | x :: xs ->
        let nl = melt_ll_neq arb [ x ] in
        _scc arb (xs @ nl) (stack @ nl) (i + 1) max_depth

let _sim_scc flag re path =
  let p_ra = L.nth (L.rev path) 3 in
  let p_cl = llast path in
  let r_cl = L.filter (fun x -> llast x = p_cl) re in
  match r_cl with
  | x :: _ ->
      let p_ca = lfst x in
      let len_p_ca = String.length p_ca in
      let len_p_ra = String.length p_ra in
      if len_p_ca < len_p_ra then
        let pre = String.sub p_ra 0 len_p_ca in
        let suf = String.sub p_ra len_p_ca (len_p_ra - len_p_ca) in
        not (flag && pre = p_ca && not (String.contains suf '1'))
      else true
  | _ -> true

let harmless_scc sccpath be =
  let first = lfst sccpath in
  let binder = L.filter (fun x -> lfst x = first) be in
  match binder with
  | [] -> false
  | l :: _ ->
      let lam = llast l in
      L.mem lam (cutlist sccpath (L.length sccpath - 3))

let scc tterm max_depth sim =
  let ae = a_edges tterm in
  let lp = legal_paths tterm in
  let re = snd lp in
  let normalizing = fst lp in
  let be = b_edges tterm in
  let arb = arb_paths ae re be in
  let ce = c_edges tterm in
  let cc = melt_ll arb ce in
  let scc_l = _scc arb cc cc 0 max_depth in
  let paths =
    L.filter
      (fun x -> is_scc (term_nodes tterm) x && not (harmless_scc x be))
      (snd scc_l)
  in
  ((fst scc_l, normalizing), L.filter (_sim_scc sim re) paths)

let unavoidable_scc sccpath =
  let first = lfst sccpath in
  let last = llast sccpath in
  let first_len = String.length first in
  let last_len = String.length last in
  if first_len < last_len then false else String.sub first 0 last_len = last

(* beta-reduction *)

(** replace every var occurrence by fresh var  *)
let rec subst var fresh term =
  match term with
  | AVar (x, t) -> if x = var then AVar (fresh, t) else term
  | ALam ((xs, e), t) ->
      let xsn = if fst xs = var then (fresh, snd xs) else xs in
      ALam ((xsn, subst var fresh e), t)
  | AApp (e1, e2, t) -> AApp (subst var fresh e1, subst var fresh e2, t)

(** capture-permitting substitution  *)
let rec cpsubst var ex term =
  match term with
  | AVar (x, t) -> if x = var then ex else term
  | ALam ((xs, e), t) ->
      if var = fst xs then term else ALam ((xs, cpsubst var ex e), t)
  | AApp (e1, e2, t) -> AApp (cpsubst var ex e1, cpsubst var ex e2, t)

let counter = ref 0

let next_fresh () =
  counter := !counter + 1;
  "p_" ^ string_of_int !counter

(** capture-avoiding substitution  *)
let rec _casubst var ex term fvex =
  (* Printf.printf "_casubst: %s[%s:=%s]\n" (a_term_to_string term) var (a_term_to_string ex); *)
  match term with
  | AVar (x, t) -> if x = var then ex else term
  | ALam ((xs, e), t) ->
      if fst xs = var then term
      else if L.mem (fst xs) fvex && L.mem var (L.map vname (free_variables e))
      then
        (* rename x to fresh *)
        let f = next_fresh () in
        let rnterm = subst (fst xs) f term in
        _casubst var ex rnterm fvex
      else ALam ((xs, _casubst var ex e fvex), t)
  | AApp (e1, e2, t) ->
      AApp (_casubst var ex e1 fvex, _casubst var ex e2 fvex, t)

let casubst var ex term =
  (* Printf.printf "casubst: %s[%s:=%s]\n" (a_term_to_string term) var (a_term_to_string ex); *)
  _casubst var ex term (L.map vname (free_variables ex))

(** capture-permitting substitution  *)
let rec cpsubst var ex term =
  match term with
  | AVar (x, t) -> if x = var then ex else term
  | ALam ((xs, e), t) ->
      if fst xs = var then term else ALam ((xs, cpsubst var ex e), t)
  | AApp (e1, e2, t) -> AApp (cpsubst var ex e1, cpsubst var ex e2, t)

(* Alpha equivalence *)

let rec rename_free_var term x new_name =
  match term with
  | AVar (s, t) -> if s = x then AVar (new_name, t) else term
  | ALam ((xs, e), t) ->
      if x = fst xs then term else ALam ((xs, rename_free_var e x new_name), t)
  | AApp (e1, e2, t) ->
      AApp (rename_free_var e1 x new_name, rename_free_var e2 x new_name, t)

let rec default_names_r term pos =
  match term with
  | AVar (s, t) -> AVar (s, t)
  | ALam ((xs, e), t) ->
      ALam
        ( ( ("x_" ^ pos, snd xs),
            default_names_r (rename_free_var e (fst xs) ("x_" ^ pos)) (pos ^ "0")
          ),
          t )
  | AApp (e1, e2, t) ->
      AApp (default_names_r e1 (pos ^ "0"), default_names_r e2 (pos ^ "1"), t)

let default_names term = default_names_r term "e"

let beta subst term =
  (* Printf.printf "beta: %s\n" (a_term_to_string term); *)
  match term with
  | AApp (ALam (((var,_), e1), _), e2, _) ->
    (* Printf.printf "subst: %s by %s in %s\n" var (a_term_to_string e2) (a_term_to_string e1); *)
    let res = subst var e2 e1 in
    (* Printf.printf "res: %s\n" (a_term_to_string res); *)
    res
  | _ -> failwith "beta: Not a redex."

let rec _reduce_at_pos subst term pos current =
  (* Printf.printf "reduce at pos %s, current %s\n" pos current; *)
  match term with
  | AVar (s, t) -> term
  | ALam ((xs, e), t) ->
      ALam ((xs, _reduce_at_pos subst e pos (current ^ "0")), t)
  | AApp (e1, e2, t) ->
      if pos = current then beta subst term
      else if is_prefix (current ^ "0") pos then
        AApp (_reduce_at_pos subst e1 pos (current ^ "0"), e2, t)
      else AApp (e1, _reduce_at_pos subst e2 pos (current ^ "1"), t)

let reduce_at_pos subst term pos = _reduce_at_pos subst term pos "e"

let rec _reduce_lo subst term =
  match term with
  | AVar (s, t) -> term
  | ALam ((xs, e), t) -> ALam ((xs, _reduce_lo subst e), t)
  | AApp (e1, e2, t) -> (
      match e1 with
      | ALam _ -> beta subst term
      | _ ->
          let left = _reduce_lo subst e1 in
          if left = e1 then AApp (e1, _reduce_lo subst e2, t)
          else AApp (left, e2, t) )

let reduce_lo subst term = _reduce_lo subst term

let rec _extract_first_redex_pos path =
  match path with
  | [] -> []
  | (pa, AS _, _) :: (pl, LS _, _) :: xs ->
      if pa ^ "0" = pl then [ pa ] else _extract_first_redex_pos xs
  | (pl, LS _, _) :: (pa, AS _, _) :: xs ->
      if pa ^ "0" = pl then [ pa ] else _extract_first_redex_pos xs
  | x :: xs -> _extract_first_redex_pos xs

let extract_first_redex_pos path = _extract_first_redex_pos path

let reduce_scc term scc_path =
  (* Printf.printf "reduce_scc %s \n" (a_term_to_string term); *)
  let rpos = extract_first_redex_pos scc_path in
  let subst = casubst in
  match rpos with
  | [] -> term
  | x :: _ ->
      (* Printf.printf "Reduce at %s \n" x; *)
      let red = reduce_at_pos subst term x in
      (* Printf.printf "reduce_scc: %s\n" (a_term_to_string red) ; *)
      red

let rec _sn_reduce_to_nf subst term =
  let new_term = reduce_lo subst term in
  if new_term = term then [] else new_term :: _sn_reduce_to_nf subst new_term

let sn_reduce_to_nf subst term = term :: _sn_reduce_to_nf subst term

let rec _reduce_to_nf term max_depth i =
  let subst = casubst in
  let new_term = reduce_lo subst term in
  if new_term = term || max_depth < i then []
  else new_term :: _reduce_to_nf new_term max_depth (i + 1)

let reduce_to_nf term max_depth = term :: _reduce_to_nf term max_depth 0

let rec reduce_with_paths term max_depth sim =
  let nodes = term_nodes term in
  let paths = scc term max_depth sim in
  (* Printf.printf "reduce_with_paths: %s %d\n" (a_term_to_string term) (L.length (snd paths)); *)
  match paths with
  | _, [] -> [ term ]
  | _, x :: _ ->
      let sym_x = L.map (fun pos -> L.hd (get_node pos nodes)) x in
      let newterm = reduce_scc term sym_x in
      if newterm = term then []
      else term :: reduce_with_paths newterm (max_depth - 1) sim

let rec sn_reduce_with_paths_to_nf term max_depth sim =
  let nodes = term_nodes term in
  let paths = scc term max_depth sim in
  let subst = casubst in
  match paths with
  | _, [] -> sn_reduce_to_nf subst term
  | _, x :: _ ->
      let sym_x = L.map (fun pos -> L.hd (get_node pos nodes)) x in
      let newterm = reduce_scc term sym_x in
      if newterm = term then []
      else term :: sn_reduce_with_paths_to_nf newterm max_depth sim

let rec size term =
  match term with
  | AVar (s, t) -> 0
  | ALam ((xs, e), t) -> 1 + size e
  | AApp (e1, e2, t) -> 1 + size e1 + size e2

let rec nf subst term =
  (* Printf.printf "%d\n" (size term); *)
  let new_term = reduce_lo subst term in
  if new_term = term then term else nf subst new_term

let is_linear term =
  let be = b_edges term in
  not (Util.duplicates (List.map (fun x -> List.hd (List.rev x)) be))