high-level abstractions for logic expressions

views.ml

type 'a view =
  | Var of string
  | App of 'a * 'a list
  | Lam of string * 'a

module T : sig
  type t
  val view : t -> t view
  val var : string -> t
  val app : t -> t list -> t
  val lam : string -> t -> t
  val fold : ('a view -> 'a) -> t -> 'a
  val pp : Format.formatter -> t -> unit
end = struct
  type t = { view: t view }
  let view x = x.view
  let var i = {view=Var i}
  let app f l = if l==[] then f else {view=App (f,l)}
  let lam x t = {view=Lam(x,t)}
  let rec fold f t = match t.view with
    | (Var _) as v -> f v
    | App (hd, l) -> f (App (fold f hd, List.map (fold f) l))
    | Lam (v, t) -> f (Lam (v, fold f t))
  let to_string = fold
    (function
      | Var v -> v
      | App (f, l) -> Printf.sprintf "(%s %s)" f (String.concat " " l)
      | Lam (x, t) -> Printf.sprintf "\\%s. %s" x t
    )
  let pp oc t = Format.pp_print_string oc (to_string t)
end

#install_printer T.pp;;

(* view of depth 2 *)
let view2 t = match T.view t with
  | Var x -> Var x
  | App (f, l) -> App (T.view f, List.map T.view l)
  | Lam (x, t) -> Lam (x, T.view t)

let t = T.(lam "x" (app (var "f") [var "x"; app (var "g") [var "b"]])) ;;

T.view t;;  (* efficient view, depth 1 *)
view2 t ;;  (* able to match deeper *)

module VarSet = Set.Make(String)                                                  
                                                                                   
let vars t =                                                                       
  T.fold                                                                           
    (fun t set -> match t with                                                     
      | Var v -> VarSet.add v set                                                  
      | Lam (v, t) -> VarSet.add v (t set)                                         
      | App (f, l) -> List.fold_right (@@) l (f set)                               
    ) t VarSet.empty