proof_checker/lib/kernel/term.ml

type var = int

type t =
  | Var of var
  | Const of string
  | Free of string
  | Function of string * t list

type match_result = AllSubst of t | SomeSubst of t | NoneSubst | MatchErr

let merge_result m1 m2 =
  match (m1, m2) with
  | AllSubst t1, AllSubst t2 -> if t1 = t2 then AllSubst t1 else MatchErr
  | AllSubst t1, SomeSubst _ -> SomeSubst t1
  | SomeSubst _, AllSubst t2 -> SomeSubst t2
  | SomeSubst t1, SomeSubst t2 -> if t1 = t2 then SomeSubst t1 else MatchErr
  | NoneSubst, _ -> m2
  | _, NoneSubst -> m1
  | _ -> MatchErr

let rec match_term x t1 t2 =
  if x = t1 then if t1 = t2 then SomeSubst t2 else AllSubst t2
  else
    match (t1, t2) with
    | Var v1, Var v2 -> if v1 = v2 then NoneSubst else MatchErr
    | Const s1, Const s2 -> if s1 = s2 then NoneSubst else MatchErr
    | Free s1, Free s2 -> if s1 = s2 then NoneSubst else MatchErr
    | Function (f1, ts1), Function (f2, ts2) ->
        if f1 = f2 && List.(length ts1 = length ts2) then
          List.(map2 (match_term x) ts1 ts2 |> fold_left merge_result NoneSubst)
        else MatchErr
    | _ -> MatchErr

let rec inc_var = function
  | Var v -> Var (v + 1)
  | Const s -> Const s
  | Free s -> Free s
  | Function (f, ts) -> Function (f, List.map inc_var ts)

let rec occurs t = function
  | Function (_, ts) -> List.exists (occurs t) ts
  | s -> t = s

let to_string binders =
  let open Format in
  let rec aux = function
    | Var v -> List.nth binders v
    | Const c -> c
    | Free f -> f
    | Function (f, args) ->
        sprintf "%s(%s)" f (String.concat ", " (List.map aux args))
  in
  aux