term.ml

(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Util
open Ident
open Ty

(** Variable symbols *)

type vsymbol = {
  vs_name : ident;
  vs_ty   : ty;
}

module Vsym = StructMake (struct
  type t = vsymbol
  let tag vs = vs.vs_name.id_tag
end)

module Svs = Vsym.S
module Mvs = Vsym.M
module Hvs = Vsym.H

let vs_equal = (==)

let create_vsymbol name ty = {
  vs_name = id_register name;
  vs_ty   = ty;
}

let fresh_vsymbol v = create_vsymbol (id_dup v.vs_name) v.vs_ty

(** Function and predicate symbols *)

type lsymbol = {
  ls_name   : ident;
  ls_args   : ty list;
  ls_value  : ty option;
}

module Lsym = StructMake (struct
  type t = lsymbol
  let tag ls = ls.ls_name.id_tag
end)

module Sls = Lsym.S
module Mls = Lsym.M
module Hls = Lsym.H

let ls_equal = (==)

let create_lsymbol name args value = {
  ls_name   = id_register name;
  ls_args   = args;
  ls_value  = value;
}

let create_fsymbol nm al vl = create_lsymbol nm al (Some vl)
let create_psymbol nm al    = create_lsymbol nm al (None)

(** Patterns *)

type pattern = {
  pat_node : pattern_node;
  pat_vars : Svs.t;
  pat_ty : ty;
  pat_tag : int;
}

and pattern_node =
  | Pwild
  | Pvar of vsymbol
  | Papp of lsymbol * pattern list
  | Por  of pattern * pattern
  | Pas  of pattern * vsymbol

let pat_equal = (==)

module Hspat = Hashcons.Make (struct
  type t = pattern

  let equal_node p1 p2 = match p1, p2 with
    | Pwild, Pwild -> true
    | Pvar v1, Pvar v2 -> vs_equal v1 v2
    | Papp (s1, l1), Papp (s2, l2) ->
        ls_equal s1 s2 && List.for_all2 pat_equal l1 l2
    | Por (p1, q1), Por (p2, q2) ->
        pat_equal p1 p2 && pat_equal q1 q2
    | Pas (p1, n1), Pas (p2, n2) ->
        pat_equal p1 p2 && vs_equal n1 n2
    | _ -> false

  let equal p1 p2 =
    equal_node p1.pat_node p2.pat_node && ty_equal p1.pat_ty p2.pat_ty

  let hash_pattern p = p.pat_tag

  let hash_node = function
    | Pwild -> 0
    | Pvar v -> v.vs_name.id_tag
    | Papp (s, pl) -> Hashcons.combine_list hash_pattern s.ls_name.id_tag pl
    | Por (p, q) -> Hashcons.combine (hash_pattern p) (hash_pattern q)
    | Pas (p, v) -> Hashcons.combine (hash_pattern p) v.vs_name.id_tag

  let hash p = Hashcons.combine (hash_node p.pat_node) p.pat_ty.ty_tag

  let tag n p = { p with pat_tag = n }
end)

module Pat = StructMake (struct
  type t = pattern
  let tag pat = pat.pat_tag
end)

module Spat = Pat.S
module Mpat = Pat.M
module Hpat = Pat.H

(* h-consing constructors for patterns *)

let mk_pattern n vs ty = Hspat.hashcons {
  pat_node = n;
  pat_vars = vs;
  pat_ty   = ty;
  pat_tag  = -1
}

exception UncoveredVar of vsymbol
exception DuplicateVar of vsymbol

let add_no_dup vs s =
  if Svs.mem vs s then raise (DuplicateVar vs) else Svs.add vs s

let pat_wild ty = mk_pattern Pwild Svs.empty ty
let pat_var v   = mk_pattern (Pvar v) (Svs.singleton v) v.vs_ty
let pat_as p v  = mk_pattern (Pas (p,v)) (add_no_dup v p.pat_vars) v.vs_ty

let pat_or p q =
  if Svs.equal p.pat_vars q.pat_vars then
    mk_pattern (Por (p,q)) p.pat_vars p.pat_ty
  else
    let s1, s2 = p.pat_vars, q.pat_vars in
    let vs = Svs.choose (Svs.union (Svs.diff s1 s2) (Svs.diff s2 s1)) in
    raise (UncoveredVar vs)

let pat_app f pl ty =
  let merge s p = Svs.fold add_no_dup s p.pat_vars in
  mk_pattern (Papp (f,pl)) (List.fold_left merge Svs.empty pl) ty

(* generic traversal functions *)

let pat_map fn pat = match pat.pat_node with
  | Pwild | Pvar _ -> pat
  | Papp (s, pl) -> pat_app s (List.map fn pl) pat.pat_ty
  | Pas (p, v) -> pat_as (fn p) v
  | Por (p, q) -> pat_or (fn p) (fn q)

let check_ty_equal ty1 ty2 =
  if not (ty_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))

let protect fn pat =
  let res = fn pat in
  check_ty_equal pat.pat_ty res.pat_ty;
  res

let pat_map fn = pat_map (protect fn)

let pat_fold fn acc pat = match pat.pat_node with
  | Pwild | Pvar _ -> acc
  | Papp (_, pl) -> List.fold_left fn acc pl
  | Pas (p, _) -> fn acc p
  | Por (p, q) -> fn (fn acc p) q

let pat_all pr pat =
  try pat_fold (all_fn pr) true pat with FoldSkip -> false

let pat_any pr pat =
  try pat_fold (any_fn pr) false pat with FoldSkip -> true

(* smart constructors for patterns *)

exception BadArity of lsymbol * int * int
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol

let pat_app fs pl ty =
  let s = match fs.ls_value with
    | Some vty -> ty_match Mtv.empty vty ty
    | None -> raise (FunctionSymbolExpected fs)
  in
  let mtch s ty p = ty_match s ty p.pat_ty in
  ignore (try List.fold_left2 mtch s fs.ls_args pl
    with Invalid_argument _ -> raise (BadArity
      (fs, List.length fs.ls_args, List.length pl)));
  pat_app fs pl ty

let pat_as p v =
  check_ty_equal p.pat_ty v.vs_ty;
  pat_as p v

let pat_or p q =
  check_ty_equal p.pat_ty q.pat_ty;
  pat_or p q

(* symbol-wise map/fold *)

let rec pat_gen_map fnT fnV fnL pat =
  let fn p = pat_gen_map fnT fnV fnL p in
  let ty = fnT pat.pat_ty in
  match pat.pat_node with
    | Pwild -> pat_wild ty
    | Pvar v -> pat_var (fnV v ty)
    | Papp (s, pl) -> pat_app (fnL s) (List.map fn pl) ty
    | Pas (p, v) -> pat_as (fn p) (fnV v ty)
    | Por (p, q) -> pat_or (fn p) (fn q)

let rec pat_gen_fold fnT fnV fnL acc pat =
  let fn acc p = pat_gen_fold fnT fnV fnL acc p in
  let acc = fnT acc pat.pat_ty in
  match pat.pat_node with
    | Pwild -> acc
    | Pvar v -> fnV acc v
    | Papp (s, pl) -> List.fold_left fn (fnL acc s) pl
    | Por (p, q) -> fn (fn acc p) q
    | Pas (p, v) -> fn (fnV acc v) p

(** Terms and formulas *)

type label = string

type quant =
  | Fforall
  | Fexists

type binop =
  | Fand
  | For
  | Fimplies
  | Fiff

type real_constant =
  | RConstDecimal of string * string * string option (* int / frac / exp *)
  | RConstHexa of string * string * string

type constant =
  | ConstInt of string
  | ConstReal of real_constant

type term = {
  t_node : term_node;
  t_label : label list;
  t_ty : ty;
  t_tag : int;
}

and fmla = {
  f_node : fmla_node;
  f_label : label list;
  f_tag : int;
}

and term_node =
  | Tbvar of int
  | Tvar of vsymbol
  | Tconst of constant
  | Tapp of lsymbol * term list
  | Tif of fmla * term * term
  | Tlet of term * term_bound
  | Tcase of term * term_branch list
  | Teps of fmla_bound

and fmla_node =
  | Fapp of lsymbol * term list
  | Fquant of quant * fmla_quant
  | Fbinop of binop * fmla * fmla
  | Fnot of fmla
  | Ftrue
  | Ffalse
  | Fif of fmla * fmla * fmla
  | Flet of term * fmla_bound
  | Fcase of term * fmla_branch list

and term_bound  = vsymbol * bind_info * term
and fmla_bound  = vsymbol * bind_info * fmla

and term_branch = pattern * bind_info * term
and fmla_branch = pattern * bind_info * fmla

and fmla_quant  = vsymbol list * bind_info * trigger list * fmla

and bind_info = {
  bv_bound : int;         (* properly bound and inst-deferred indices *)
  bv_open  : Sint.t;      (* externally visible indices *)
  bv_defer : term Mint.t  (* deferred instantiation *)
}

and trigger = expr list

and expr =
  | Term of term
  | Fmla of fmla

(* term and fmla equality *)

let t_equal = (==)
let f_equal = (==)

(* expr and trigger equality *)

let e_equal e1 e2 = match e1, e2 with
  | Term t1, Term t2 -> t_equal t1 t2
  | Fmla f1, Fmla f2 -> f_equal f1 f2
  | _ -> false

let tr_equal = list_all2 (list_all2 e_equal)

(* expr and trigger traversal *)

let e_map fnT fnF = function Term t -> Term (fnT t) | Fmla f -> Fmla (fnF f)
let e_fold fnT fnF acc = function Term t -> fnT acc t | Fmla f -> fnF acc f
let e_apply fnT fnF = function Term t -> fnT t | Fmla f -> fnF f

let e_map_fold fnT fnF acc = function
  | Term t -> let acc, t = fnT acc t in acc, Term t
  | Fmla f -> let acc, f = fnF acc f in acc, Fmla f

let tr_map fnT fnF = List.map (List.map (e_map fnT fnF))
let tr_fold fnT fnF = List.fold_left (List.fold_left (e_fold fnT fnF))

let tr_map_fold fnT fnF =
  Util.map_fold_left (Util.map_fold_left (e_map_fold fnT fnF))

(* bind_info equality, hash, and traversal *)

let bnd_equal b1 b2 =
  b1.bv_bound = b2.bv_bound && Mint.equal t_equal b1.bv_defer b2.bv_defer

let bnd_hash bv =
  Mint.fold (fun i t a -> Hashcons.combine2 i t.t_tag a) bv.bv_defer

let bnd_map fn bv = { bv with bv_defer = Mint.map fn bv.bv_defer }
let bnd_fold fn acc bv = Mint.fold (fun _ t a -> fn a t) bv.bv_defer acc

let bnd_map_fold fn acc bv =
  let acc,s = Mint.fold
    (fun i t (a,b) -> let a,t = fn a t in a, Mint.add i t b)
    bv.bv_defer (acc, Mint.empty)
  in
  acc, { bv with bv_defer = s }

(* hash-consing for terms and formulas *)

module Hsterm = Hashcons.Make (struct

  type t = term

  let t_eq_branch (p1,b1,t1) (p2,b2,t2) =
    pat_equal p1 p2 && bnd_equal b1 b2 && t_equal t1 t2

  let t_eq_bound (v1,b1,t1) (v2,b2,t2) =
    vs_equal v1 v2 && bnd_equal b1 b2 && t_equal t1 t2

  let f_eq_bound (v1,b1,f1) (v2,b2,f2) =
    vs_equal v1 v2 && bnd_equal b1 b2 && f_equal f1 f2

  let t_equal_node t1 t2 = match t1,t2 with
    | Tbvar x1, Tbvar x2 -> x1 = x2
    | Tvar v1, Tvar v2 -> vs_equal v1 v2
    | Tconst c1, Tconst c2 -> c1 = c2
    | Tapp (s1,l1), Tapp (s2,l2) ->
        ls_equal s1 s2 && List.for_all2 t_equal l1 l2
    | Tif (f1,t1,e1), Tif (f2,t2,e2) ->
        f_equal f1 f2 && t_equal t1 t2 && t_equal e1 e2
    | Tlet (t1,b1), Tlet (t2,b2) ->
        t_equal t1 t2 && t_eq_bound b1 b2
    | Tcase (t1,bl1), Tcase (t2,bl2) ->
        t_equal t1 t2 && list_all2 t_eq_branch bl1 bl2
    | Teps f1, Teps f2 -> f_eq_bound f1 f2
    | _ -> false

  let equal t1 t2 =
    t_equal t1.t_ty t2.t_ty &&
    t_equal_node t1.t_node t2.t_node &&
    list_all2 (=) t1.t_label t2.t_label

  let t_hash_branch (p,b,t) =
    Hashcons.combine p.pat_tag (bnd_hash b t.t_tag)

  let t_hash_bound (v,b,t) =
    Hashcons.combine v.vs_name.id_tag (bnd_hash b t.t_tag)

  let f_hash_bound (v,b,f) =
    Hashcons.combine v.vs_name.id_tag (bnd_hash b f.f_tag)

  let t_hash t = t.t_tag

  let t_hash_node = function
    | Tbvar n -> n
    | Tvar v -> v.vs_name.id_tag
    | Tconst c -> Hashtbl.hash c
    | Tapp (f,tl) -> Hashcons.combine_list t_hash (f.ls_name.id_tag) tl
    | Tif (f,t,e) -> Hashcons.combine2 f.f_tag t.t_tag e.t_tag
    | Tlet (t,bt) -> Hashcons.combine t.t_tag (t_hash_bound bt)
    | Tcase (t,bl) -> Hashcons.combine_list t_hash_branch t.t_tag bl
    | Teps f -> f_hash_bound f

  let hash t =
    Hashcons.combine (t_hash_node t.t_node)
      (Hashcons.combine_list Hashtbl.hash t.t_ty.ty_tag t.t_label)

  let tag n t = { t with t_tag = n }

end)

module Term = StructMake (struct
  type t = term
  let tag term = term.t_tag
end)

module Sterm = Term.S
module Mterm = Term.M
module Hterm = Term.H

module Hsfmla = Hashcons.Make (struct

  type t = fmla

  let f_eq_branch (p1,b1,f1) (p2,b2,f2) =
    pat_equal p1 p2 && bnd_equal b1 b2 && f_equal f1 f2

  let f_eq_bound (v1,b1,f1) (v2,b2,f2) =
    vs_equal v1 v2 && bnd_equal b1 b2 && f_equal f1 f2

  let f_eq_quant (vl1,b1,tl1,f1) (vl2,b2,tl2,f2) =
    f_equal f1 f2 && list_all2 vs_equal vl1 vl2 &&
    bnd_equal b1 b2 && tr_equal tl1 tl2

  let f_equal_node f1 f2 = match f1,f2 with
    | Fapp (s1,l1), Fapp (s2,l2) ->
        ls_equal s1 s2 && List.for_all2 t_equal l1 l2
    | Fquant (q1,b1), Fquant (q2,b2) ->
        q1 = q2 && f_eq_quant b1 b2
    | Fbinop (op1,f1,g1), Fbinop (op2,f2,g2) ->
        op1 = op2 && f_equal f1 f2 && f_equal g1 g2
    | Fnot f1, Fnot f2 -> f_equal f1 f2
    | Ftrue, Ftrue | Ffalse, Ffalse -> true
    | Fif (f1,g1,h1), Fif (f2,g2,h2) ->
        f_equal f1 f2 && f_equal g1 g2 && f_equal h1 h2
    | Flet (t1,b1), Flet (t2,b2) ->
        t_equal t1 t2 && f_eq_bound b1 b2
    | Fcase (t1,bl1), Fcase (t2,bl2) ->
        t_equal t1 t2 && list_all2 f_eq_branch bl1 bl2
    | _ -> false

  let equal f1 f2 =
    f_equal_node f1.f_node f2.f_node &&
    list_all2 (=) f1.f_label f2.f_label

  let v_hash v = v.vs_name.id_tag

  let t_hash t = t.t_tag

  let f_hash_branch (p,b,f) =
    Hashcons.combine p.pat_tag (bnd_hash b f.f_tag)

  let f_hash_bound (v,b,f) =
    Hashcons.combine v.vs_name.id_tag (bnd_hash b f.f_tag)

  let tr_hash = function Term t -> t.t_tag | Fmla f -> f.f_tag

  let f_hash_quant (vl,b,tl,f) =
    let h = bnd_hash b f.f_tag in
    let h = Hashcons.combine_list v_hash h vl in
    List.fold_left (Hashcons.combine_list tr_hash) h tl

  let f_hash_node = function
    | Fapp (p,tl) -> Hashcons.combine_list t_hash p.ls_name.id_tag tl
    | Fquant (q,bf) -> Hashcons.combine (Hashtbl.hash q) (f_hash_quant bf)
    | Fbinop (op,f1,f2) ->
        Hashcons.combine2 (Hashtbl.hash op) f1.f_tag f2.f_tag
    | Fnot f -> Hashcons.combine 1 f.f_tag
    | Ftrue -> 0
    | Ffalse -> 1
    | Fif (f1,f2,f3) -> Hashcons.combine2 f1.f_tag f2.f_tag f3.f_tag
    | Flet (t,bf) -> Hashcons.combine t.t_tag (f_hash_bound bf)
    | Fcase (t,bl) -> Hashcons.combine_list f_hash_branch t.t_tag bl

  let hash f =
    Hashcons.combine_list Hashtbl.hash (f_hash_node f.f_node) f.f_label

  let tag n f = { f with f_tag = n }

end)

module Fmla = StructMake (struct
  type t = fmla
  let tag fmla = fmla.f_tag
end)

module Sfmla = Fmla.S
module Mfmla = Fmla.M
module Hfmla = Fmla.H

(* hash-consing constructors for terms *)

let mk_term n ty = Hsterm.hashcons {
  t_node = n; t_label = []; t_ty = ty; t_tag = -1 }

let t_bvar n ty     = mk_term (Tbvar n) ty
let t_var v         = mk_term (Tvar v) v.vs_ty
let t_const c ty    = mk_term (Tconst c) ty
let t_int_const s   = mk_term (Tconst (ConstInt s)) Ty.ty_int
let t_real_const r  = mk_term (Tconst (ConstReal r)) Ty.ty_real
let t_app f tl ty   = mk_term (Tapp (f, tl)) ty
let t_if f t1 t2    = mk_term (Tif (f, t1, t2)) t2.t_ty
let t_let t1 bt ty  = mk_term (Tlet (t1, bt)) ty
let t_case t1 bl ty = mk_term (Tcase (t1, bl)) ty
let t_eps bf ty     = mk_term (Teps bf) ty

let t_label     l t = Hsterm.hashcons { t with t_label = l }
let t_label_add l t = Hsterm.hashcons { t with t_label = l :: t.t_label }

let t_label_copy { t_label = l } t =
  if t.t_label = [] && l <> [] then t_label l t else t

(* hash-consing constructors for formulas *)

let mk_fmla n = Hsfmla.hashcons { f_node = n; f_label = []; f_tag = -1 }

let f_app f tl        = mk_fmla (Fapp (f, tl))
let f_quant q qf      = mk_fmla (Fquant (q, qf))
let f_binary op f1 f2 = mk_fmla (Fbinop (op, f1, f2))
let f_not f           = mk_fmla (Fnot f)
let f_true            = mk_fmla (Ftrue)
let f_false           = mk_fmla (Ffalse)
let f_if f1 f2 f3     = mk_fmla (Fif (f1, f2, f3))
let f_let t bf        = mk_fmla (Flet (t, bf))
let f_case t bl       = mk_fmla (Fcase (t, bl))

let f_label     l f = Hsfmla.hashcons { f with f_label = l }
let f_label_add l f = Hsfmla.hashcons { f with f_label = l :: f.f_label }

let f_label_copy { f_label = l } f =
  if f.f_label = [] && l <> [] then f_label l f else f

let f_and     = f_binary Fand
let f_or      = f_binary For
let f_implies = f_binary Fimplies
let f_iff     = f_binary Fiff

(* built-in symbols *)

let ps_equ =
  let v = ty_var (create_tvsymbol (id_fresh "a")) in
  create_psymbol (id_fresh "infix =") [v; v]

let ps_neq =
  let v = ty_var (create_tvsymbol (id_fresh "a")) in
  create_psymbol (id_fresh "infix <>") [v; v]

let f_app p tl =
  if ls_equal p ps_neq then f_not (f_app ps_equ tl) else f_app p tl

let f_equ t1 t2 = f_app ps_equ [t1; t2]
let f_neq t1 t2 = f_app ps_neq [t1; t2]

let fs_tuple n =
  let tyl = ref [] in
  for i = 1 to n
  do tyl := ty_var (create_tvsymbol (id_fresh "a")) :: !tyl done;
  let ty = ty_tuple !tyl in
  create_fsymbol (id_fresh ("Tuple" ^ string_of_int n)) !tyl ty

let fs_tuple = Util.memo fs_tuple

let is_fs_tuple fs = fs == fs_tuple (List.length fs.ls_args)

let t_tuple tl =
  let ty = ty_tuple (List.map (fun t -> t.t_ty) tl) in
  t_app (fs_tuple (List.length tl)) tl ty

(* unsafe map *)

let bound_map fnT fnE (u,b,e) = (u, bnd_map fnT b, fnE e)

let t_map_unsafe fnT fnF t = t_label_copy t (match t.t_node with
  | Tbvar _ | Tvar _ | Tconst _ -> t
  | Tapp (f,tl) -> t_app f (List.map fnT tl) t.t_ty
  | Tif (f,t1,t2) -> t_if (fnF f) (fnT t1) (fnT t2)
  | Tlet (e,b) -> t_let (fnT e) (bound_map fnT fnT b) t.t_ty
  | Tcase (e,bl) -> t_case (fnT e) (List.map (bound_map fnT fnT) bl) t.t_ty
  | Teps b -> t_eps (bound_map fnT fnF b) t.t_ty)

let f_map_unsafe fnT fnF f = f_label_copy f (match f.f_node with
  | Fapp (p,tl) -> f_app p (List.map fnT tl)
  | Fquant (q,(vl,b,tl,f1)) ->
      f_quant q (vl, bnd_map fnT b, tr_map fnT fnF tl, fnF f1)
  | Fbinop (op,f1,f2) -> f_binary op (fnF f1) (fnF f2)
  | Fnot f1 -> f_not (fnF f1)
  | Ftrue | Ffalse -> f
  | Fif (f1,f2,f3) -> f_if (fnF f1) (fnF f2) (fnF f3)
  | Flet (e,b) -> f_let (fnT e) (bound_map fnT fnF b)
  | Fcase (e,bl) -> f_case (fnT e) (List.map (bound_map fnT fnF) bl))

(* unsafe fold *)

let bound_fold fnT fnE acc (_,b,e) = fnE (bnd_fold fnT acc b) e

let t_fold_unsafe fnT fnF acc t = match t.t_node with
  | Tbvar _ | Tvar _ | Tconst _ -> acc
  | Tapp (_,tl) -> List.fold_left fnT acc tl
  | Tif (f,t1,t2) -> fnT (fnT (fnF acc f) t1) t2
  | Tlet (e,b) -> fnT (bound_fold fnT fnT acc b) e
  | Tcase (e,bl) -> List.fold_left (bound_fold fnT fnT) (fnT acc e) bl
  | Teps b -> bound_fold fnT fnF acc b

let f_fold_unsafe fnT fnF acc f = match f.f_node with
  | Fapp (_,tl) -> List.fold_left fnT acc tl
  | Fquant (_,(_,b,tl,f1)) -> fnF (tr_fold fnT fnF (bnd_fold fnT acc b) tl) f1
  | Fbinop (_,f1,f2) -> fnF (fnF acc f1) f2
  | Fnot f1 -> fnF acc f1
  | Ftrue | Ffalse -> acc
  | Fif (f1,f2,f3) -> fnF (fnF (fnF acc f1) f2) f3
  | Flet (e,b) -> fnT (bound_fold fnT fnF acc b) e
  | Fcase (e,bl) -> List.fold_left (bound_fold fnT fnF) (fnT acc e) bl

let all_fnT prT _ t = prT t || raise FoldSkip
let all_fnF prF _ f = prF f || raise FoldSkip
let any_fnT prT _ t = prT t && raise FoldSkip
let any_fnF prF _ f = prF f && raise FoldSkip

let t_all_unsafe prT prF t =
  try t_fold_unsafe (all_fnT prT) (all_fnF prF) true t
  with FoldSkip -> false

let f_all_unsafe prT prF f =
  try f_fold_unsafe (all_fnT prT) (all_fnF prF) true f
  with FoldSkip -> false

let t_any_unsafe prT prF t =
  try t_fold_unsafe (any_fnT prT) (any_fnF prF) false t
  with FoldSkip -> true

let f_any_unsafe prT prF f =
  try f_fold_unsafe (any_fnT prT) (any_fnF prF) false f
  with FoldSkip -> true

(* unsafe map_fold *)

let bound_map_fold fnT fnE acc (u,b,e) =
  let acc, b = bnd_map_fold fnT acc b in
  let acc, e = fnE acc e in
  acc, (u,b,e)

let t_map_fold_unsafe fnT fnF acc t = match t.t_node with
  | Tbvar _ | Tvar _ | Tconst _ ->
      acc, t
  | Tapp (f,tl) ->
      let acc,tl = map_fold_left fnT acc tl in
      acc, t_label_copy t (t_app f tl t.t_ty)
  | Tif (f,t1,t2) ->
      let acc, f  = fnF acc f in
      let acc, t1 = fnT acc t1 in
      let acc, t2 = fnT acc t2 in
      acc, t_label_copy t (t_if f t1 t2)
  | Tlet (e,b) ->
      let acc, e = fnT acc e in
      let acc, b = bound_map_fold fnT fnT acc b in
      acc, t_label_copy t (t_let e b t.t_ty)
  | Tcase (e,bl) ->
      let acc, e = fnT acc e in
      let acc, bl = map_fold_left (bound_map_fold fnT fnT) acc bl in
      acc, t_label_copy t (t_case e bl t.t_ty)
  | Teps b ->
      let acc, b = bound_map_fold fnT fnF acc b in
      acc, t_label_copy t (t_eps b t.t_ty)

let f_map_fold_unsafe fnT fnF acc f = match f.f_node with
  | Fapp (p,tl) ->
      let acc,tl = map_fold_left fnT acc tl in
      acc, f_label_copy f (f_app p tl)
  | Fquant (q,(vl,b,tl,f1)) ->
      let acc, b = bnd_map_fold fnT acc b in
      let acc, tl = tr_map_fold fnT fnF acc tl in
      let acc, f1 = fnF acc f1 in
      acc, f_label_copy f (f_quant q (vl,b,tl,f1))
  | Fbinop (op,f1,f2) ->
      let acc, f1 = fnF acc f1 in
      let acc, f2 = fnF acc f2 in
      acc, f_label_copy f (f_binary op f1 f2)
  | Fnot f1 ->
      let acc, f1 = fnF acc f1 in
      acc, f_label_copy f (f_not f1)
  | Ftrue | Ffalse ->
      acc, f
  | Fif (f1,f2,f3) ->
      let acc, f1 = fnF acc f1 in
      let acc, f2 = fnF acc f2 in
      let acc, f3 = fnF acc f3 in
      acc, f_label_copy f (f_if f1 f2 f3)
  | Flet (e,b) ->
      let acc, e = fnT acc e in
      let acc, b = bound_map_fold fnT fnF acc b in
      acc, f_label_copy f (f_let e b)
  | Fcase (e,bl) ->
      let acc, e = fnT acc e in
      let acc, bl = map_fold_left (bound_map_fold fnT fnF) acc bl in
      acc, f_label_copy f (f_case e bl)

(* replaces variables with de Bruijn indices in term [t] using map [m] *)

let rec t_abst m l lvl t = t_label_copy t (match t.t_node with
  | Tvar u -> begin try
      let i = Mvs.find u m in
      l := Sint.add i !l;
      t_bvar (i + lvl) t.t_ty
      with Not_found -> t end
  | Tlet (e, (u,b,t1)) ->
      let b,t1 = bnd_t_abst m l lvl b t1 in
      t_let (t_abst m l lvl e) (u,b,t1) t.t_ty
  | Tcase (e, bl) ->
      let br_abst (p,b,e) = let b,e = bnd_t_abst m l lvl b e in (p,b,e) in
      t_case (t_abst m l lvl e) (List.map br_abst bl) t.t_ty
  | Teps (u,b,f) ->
      let b,f = bnd_f_abst m l lvl b f in
      t_eps (u,b,f) t.t_ty
  | _ ->
      t_map_unsafe (t_abst m l lvl) (f_abst m l lvl) t)

and f_abst m l lvl f = f_label_copy f (match f.f_node with
  | Fquant (q, qf) ->
      f_quant q (bnd_q_abst m l lvl qf)
  | Flet (e, (u,b,f1)) ->
      let b,f1 = bnd_f_abst m l lvl b f1 in
      f_let (t_abst m l lvl e) (u,b,f1)
  | Fcase (e, bl) ->
      let br_abst (p,b,e) = let b,e = bnd_f_abst m l lvl b e in (p,b,e) in
      f_case (t_abst m l lvl e) (List.map br_abst bl)
  | _ ->
      f_map_unsafe (t_abst m l lvl) (f_abst m l lvl) f)

and bnd_t_abst m l lvl bv t =
  let l' = ref Sint.empty in
  let t = t_abst m l' (lvl + bv.bv_bound) t in
  update_bv m l lvl l' bv, t

and bnd_f_abst m l lvl bv f =
  let l' = ref Sint.empty in
  let f = f_abst m l' (lvl + bv.bv_bound) f in
  update_bv m l lvl l' bv, f

and bnd_q_abst m l lvl (vl,bv,tl,f) =
  let l' = ref Sint.empty and lvl' = lvl + bv.bv_bound in
  let tl = tr_map (t_abst m l' lvl') (f_abst m l' lvl') tl in
  let f = f_abst m l' lvl' f in
  vl, update_bv m l lvl l' bv, tl, f

and update_bv m l lvl l' bv =
  l := Sint.union !l' !l;
  let bv = bnd_map (t_abst m l lvl) bv in
  let add i acc = Sint.add (i + lvl) acc in
  { bv with bv_open = Sint.fold add !l' bv.bv_open }

let t_abst m t = t_abst m (ref Sint.empty) 0 t
let f_abst m f = f_abst m (ref Sint.empty) 0 f

(* replaces de Bruijn indices with variables in term [t] using map [m] *)

exception UnboundIndex

let bnd_find i m =
  try Mint.find i m with Not_found -> raise UnboundIndex

let bnd_inst m nv { bv_bound = d ; bv_open = b ; bv_defer = s } =
  let s = Sint.fold (fun i -> Mint.add (i + d) (bnd_find i m)) b s in
  { bv_bound = d + nv ; bv_open = Sint.empty ; bv_defer = s }

let rec t_inst m nv t = t_label_copy t (match t.t_node with
  | Tbvar i ->
      bnd_find i m
  | Tlet (e,(u,b,t1)) ->
      t_let (t_inst m nv e) (u, bound_inst m nv b, t1) t.t_ty
  | Tcase (e,bl) ->
      let br_inst (u,b,e) = (u, bound_inst m nv b, e) in
      t_case (t_inst m nv e) (List.map br_inst bl) t.t_ty
  | Teps (u,b,f) ->
      t_eps (u, bound_inst m nv b, f) t.t_ty
  | _ ->
      t_map_unsafe (t_inst m nv) (f_inst m nv) t)

and f_inst m nv f = f_label_copy f (match f.f_node with
  | Fquant (q,(vl,b,tl,f)) ->
      f_quant q (vl, bound_inst m nv b, tl, f)
  | Flet (e,(u,b,f1)) ->
      f_let (t_inst m nv e) (u, bound_inst m nv b, f1)
  | Fcase (e,bl) ->
      let br_inst (u,b,e) = (u, bound_inst m nv b, e) in
      f_case (t_inst m nv e) (List.map br_inst bl)
  | _ ->
      f_map_unsafe (t_inst m nv) (f_inst m nv) f)

and bound_inst m nv b = bnd_inst m nv (bnd_map (t_inst m nv) b)

(* close bindings *)

let bnd_new nv =
  { bv_bound = nv ; bv_open = Sint.empty ; bv_defer = Mint.empty }

let t_close_bound v t = (v, bnd_new 1, t_abst (Mvs.add v 0 Mvs.empty) t)
let f_close_bound v f = (v, bnd_new 1, f_abst (Mvs.add v 0 Mvs.empty) f)

let pat_varmap p =
  let i = ref (-1) in
  let rec mk_map acc p = match p.pat_node with
    | Pvar n -> incr i; Mvs.add n !i acc
    | Pas (p, n) -> incr i; mk_map (Mvs.add n !i acc) p
    | Por (p, _) -> mk_map acc p
    | _ -> pat_fold mk_map acc p
  in
  let m = mk_map Mvs.empty p in
  m, !i + 1

let t_close_branch pat t =
  let m,nv = pat_varmap pat in
  (pat, bnd_new nv, if nv = 0 then t else t_abst m t)

let f_close_branch pat f =
  let m,nv = pat_varmap pat in
  (pat, bnd_new nv, if nv = 0 then f else f_abst m f)

let f_close_quant vl tl f =
  if vl = [] then (vl, bnd_new 0, tl, f) else
  let i = ref (-1) in
  let add m v =
    if Mvs.mem v m then raise (DuplicateVar v);
    incr i; Mvs.add v !i m
  in
  let m = List.fold_left add Mvs.empty vl in
  (vl, bnd_new (!i + 1), tr_map (t_abst m) (f_abst m) tl, f_abst m f)

(* open bindings *)

let t_open_bound (v,b,t) =
  let v = fresh_vsymbol v in
  v, t_inst (Mint.add 0 (t_var v) b.bv_defer) b.bv_bound t

let f_open_bound (v,b,f) =
  let v = fresh_vsymbol v in
  v, f_inst (Mint.add 0 (t_var v) b.bv_defer) b.bv_bound f

let rec pat_rename ns p = match p.pat_node with
  | Pvar n -> pat_var (Mvs.find n ns)
  | Pas (p, n) -> pat_as (pat_rename ns p) (Mvs.find n ns)
  | _ -> pat_map (pat_rename ns) p

let pat_substs p s =
  let m, _ = pat_varmap p in
  Mvs.fold (fun x i (s, ns) ->
    let x' = fresh_vsymbol x in
    Mint.add i (t_var x') s, Mvs.add x x' ns) m (s, Mvs.empty)

let t_open_branch (p,b,t) =
  if b.bv_bound = 0 then (p, t) else
  let m,ns = pat_substs p b.bv_defer in
  pat_rename ns p, t_inst m b.bv_bound t

let f_open_branch (p,b,f) =
  if b.bv_bound = 0 then (p, f) else
  let m,ns = pat_substs p b.bv_defer in
  pat_rename ns p, f_inst m b.bv_bound f

let quant_vars vl s =
  let i = ref (-1) in
  let add m v = let v = fresh_vsymbol v in
    incr i; Mint.add !i (t_var v) m, v in