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 mk_ls name args value = {
  ls_name   = name;
  ls_args   = args;
  ls_value  = value;
}

let lsymbol_table = Wid.create 63

let create_lsymbol name args value =
  let id = id_register name in
  let ls = mk_ls id args value in
  let wa = Weak.create 1 in
  Weak.set wa 0 (Some ls);
  Wid.set lsymbol_table id wa;
  ls

let find_lsymbol id =
  match Weak.get (Wid.find lsymbol_table id) 0 with
  | Some ls -> ls
  | None -> raise Not_found

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_ty : ty;
  pat_tag : int;
}

and pattern_node =
  | Pwild
  | Pvar of vsymbol
  | Papp of lsymbol * pattern list
  | 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
    | 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
    | 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 ty = { pat_node = n; pat_ty = ty; pat_tag = -1 }
let pat_wild ty = Hspat.hashcons (mk_pattern Pwild ty)
let pat_var v = Hspat.hashcons (mk_pattern (Pvar v) v.vs_ty)
let pat_app f pl ty = Hspat.hashcons (mk_pattern (Papp (f, pl)) ty)
let pat_as p v = Hspat.hashcons (mk_pattern (Pas (p, v)) p.pat_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

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

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

let rec pat_freevars s pat = match pat.pat_node with
  | Pwild -> s
  | Pvar v -> Svs.add v s
  | Pas (p, v) -> pat_freevars (Svs.add v s) p
  | Papp (_,pl) -> List.fold_left pat_freevars s pl

(* 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

(* symbol-wise map/fold *)

let rec pat_s_map fnT fnV fnL pat =
  let fn p = pat_s_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)

let rec pat_s_fold fnT fnL acc pat =
  let fn acc p = pat_s_fold fnT fnL acc p in
  let acc = ty_s_fold fnT acc pat.pat_ty in
  match pat.pat_node with
    | Pwild | Pvar _ -> acc
    | Papp (s, pl) -> List.fold_left fn (fnL acc s) pl
    | Pas (p, _) -> fn acc 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 list * 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 list * fmla_branch list

and term_bound = vsymbol * term

and fmla_bound = vsymbol * fmla

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

and term_branch = pattern list * int * term

and fmla_branch = pattern list * int * fmla

and expr =
  | Term of term
  | Fmla of fmla

and trigger = expr list

(* 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 e_equal
let trl_equal = list_all2 tr_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 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))

module Hsterm = Hashcons.Make (struct

  type t = term

  let t_eq_branch (pl1,_,t1) (pl2,_,t2) =
    list_all2 pat_equal pl1 pl2 && t_equal t1 t2

  let t_eq_bound (v1, t1) (v2, t2) = vs_equal v1 v2 && t_equal t1 t2
  let f_eq_bound (v1, f1) (v2, f2) = vs_equal v1 v2 && 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 (tl1, bl1), Tcase (tl2, bl2) ->
        list_all2 t_equal tl1 tl2 && list_all2 t_eq_branch bl1 bl2
    | Teps f1, Teps f2 -> f_eq_bound f1 f2
    | _ -> false

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

  let p_hash p = p.pat_tag

  let t_hash_branch (pl,_,t) = Hashcons.combine_list p_hash t.t_tag pl

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

  let f_hash_bound (v, f) = Hashcons.combine v.vs_name.id_tag 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 (tl, bl) -> let ht = Hashcons.combine_list t_hash 17 tl in
        Hashcons.combine_list t_hash_branch ht 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 (pl1,_,f1) (pl2,_,f2) =
    list_all2 pat_equal pl1 pl2 && f_equal f1 f2

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

  let f_eq_quant (vl1, _, tl1, f1) (vl2, _, tl2, f2) =
    f_equal f1 f2 && list_all2 vs_equal vl1 vl2 && trl_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 (tl1, bl1), Fcase (tl2, bl2) ->
        list_all2 t_equal tl1 tl2 && 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 p_hash p = p.pat_tag

  let t_hash t = t.t_tag

  let f_hash_branch (pl,_,f) = Hashcons.combine_list p_hash f.f_tag pl

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

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

  let f_hash_quant (vl, _, tl, f) =
    let h = Hashcons.combine_list v_hash f.f_tag 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 (tl, bl) -> let ht = Hashcons.combine_list t_hash 17 tl in
        Hashcons.combine_list f_hash_branch ht 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 v t1 t2   = mk_term (Tlet (t1, (v, t2))) t2.t_ty
let t_case tl bl ty = mk_term (Tcase (tl, bl)) ty
let t_eps u f       = mk_term (Teps (u, f)) u.vs_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 l = [] then t else t_label l t

let t_app_unsafe = t_app

(* 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 ul n tl f = mk_fmla (Fquant (q, (ul,n,tl,f)))
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 v t f         = mk_fmla (Flet (t, (v, f)))
let f_case tl bl        = mk_fmla (Fcase (tl, 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 l = [] then f else f_label l 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 f_app_unsafe = f_app

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 with level *)

exception UnboundIndex

let brlvl fn lvl (pat, nv, t) = (pat, nv, fn (lvl + nv) t)

let t_map_unsafe fnT fnF lvl t = t_label_copy t (match t.t_node with
  | Tbvar n when n >= lvl -> raise UnboundIndex
  | Tbvar _ | Tvar _ | Tconst _ -> t
  | Tapp (f, tl) -> t_app f (List.map (fnT lvl) tl) t.t_ty
  | Tif (f, t1, t2) -> t_if (fnF lvl f) (fnT lvl t1) (fnT lvl t2)
  | Tlet (t1, (u, t2)) -> t_let u (fnT lvl t1) (fnT (lvl + 1) t2)
  | Tcase (tl, bl) ->
      t_case (List.map (fnT lvl) tl) (List.map (brlvl fnT lvl) bl) t.t_ty
  | Teps (u, f) -> t_eps u (fnF (lvl + 1) f))

let f_map_unsafe fnT fnF lvl f = f_label_copy f (match f.f_node with
  | Fapp (p, tl) -> f_app p (List.map (fnT lvl) tl)
  | Fquant (q, (vl, nv, tl, f1)) -> let lvl = lvl + nv in
      f_quant q vl nv (tr_map (fnT lvl) (fnF lvl) tl) (fnF lvl f1)
  | Fbinop (op, f1, f2) -> f_binary op (fnF lvl f1) (fnF lvl f2)
  | Fnot f1 -> f_not (fnF lvl f1)
  | Ftrue | Ffalse -> f
  | Fif (f1, f2, f3) -> f_if (fnF lvl f1) (fnF lvl f2) (fnF lvl f3)
  | Flet (t, (u, f1)) -> f_let u (fnT lvl t) (fnF (lvl + 1) f1)
  | Fcase (tl, bl) ->
      f_case (List.map (fnT lvl) tl) (List.map (brlvl fnF lvl) bl))

let protect fn lvl t =
  let res = fn lvl t in
  check_ty_equal t.t_ty res.t_ty;
  res

let t_map_unsafe fnT = t_map_unsafe (protect fnT)
let f_map_unsafe fnT = f_map_unsafe (protect fnT)

(* unsafe fold with level *)

let brlvl fn lvl acc (_, nv, t) = fn (lvl + nv) acc t

let t_fold_unsafe fnT fnF lvl acc t = match t.t_node with
  | Tbvar n when n >= lvl -> raise UnboundIndex
  | Tbvar _ | Tvar _ | Tconst _ -> acc
  | Tapp (_, tl) -> List.fold_left (fnT lvl) acc tl
  | Tif (f, t1, t2) -> fnT lvl (fnT lvl (fnF lvl acc f) t1) t2
  | Tlet (t1, (_, t2)) -> fnT (lvl + 1) (fnT lvl acc t1) t2
  | Tcase (tl, bl) ->
      List.fold_left (brlvl fnT lvl) (List.fold_left (fnT lvl) acc tl) bl
  | Teps (_, f) -> fnF (lvl + 1) acc f

let f_fold_unsafe fnT fnF lvl acc f = match f.f_node with
  | Fapp (_, tl) -> List.fold_left (fnT lvl) acc tl
  | Fquant (_, (_, nv, tl, f1)) -> let lvl = lvl + nv in
      tr_fold (fnT lvl) (fnF lvl) (fnF lvl acc f1) tl
  | Fbinop (_, f1, f2) -> fnF lvl (fnF lvl acc f1) f2
  | Fnot f1 -> fnF lvl acc f1
  | Ftrue | Ffalse -> acc
  | Fif (f1, f2, f3) -> fnF lvl (fnF lvl (fnF lvl acc f1) f2) f3
  | Flet (t, (_, f1)) -> fnF (lvl + 1) (fnT lvl acc t) f1
  | Fcase (tl, bl) ->
      List.fold_left (brlvl fnF lvl) (List.fold_left (fnT lvl) acc tl) bl

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

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

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

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

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

(* unsafe constructors with type checking *)

let t_app_inst fs tl ty =
  let s = match fs.ls_value with
    | Some vty -> ty_match Mtv.empty vty ty
    | _ -> raise (FunctionSymbolExpected fs)
  in
  let mtch s ty t = ty_match s ty t.t_ty in
  try List.fold_left2 mtch s fs.ls_args tl
  with Invalid_argument _ -> raise (BadArity
    (fs, List.length fs.ls_args, List.length tl))

let t_app fs tl ty = ignore (t_app_inst fs tl ty); t_app fs tl ty

let t_app_infer fs tl =
  let mtch s ty t = ty_match s ty t.t_ty in
  let s =
    try List.fold_left2 mtch Mtv.empty fs.ls_args tl
    with Invalid_argument _ -> raise (BadArity
      (fs, List.length fs.ls_args, List.length tl))
  in
  let ty = match fs.ls_value with
    | Some ty -> ty_inst s ty
    | _ -> raise (FunctionSymbolExpected fs)
  in
  t_app_unsafe fs tl ty

let f_app_inst ps tl =
  let s = match ps.ls_value with
    | None -> Mtv.empty
    | _ -> raise (PredicateSymbolExpected ps)
  in
  let mtch s ty t = ty_match s ty t.t_ty in
  try List.fold_left2 mtch s ps.ls_args tl
  with Invalid_argument _ -> raise (BadArity
    (ps, List.length ps.ls_args, List.length tl))

let f_app ps tl = ignore (f_app_inst ps tl); f_app ps tl

let p_check t p =
  check_ty_equal p.pat_ty t.t_ty

let t_case tl bl ty =
  let t_check_branch (pl,_,tbr) =
    check_ty_equal ty tbr.t_ty;
    List.iter2 p_check tl pl
  in
  List.iter t_check_branch bl;
  t_case tl bl ty

let f_case tl bl =
  let f_check_branch (pl,_,_) =
    List.iter2 p_check tl pl
  in
  List.iter f_check_branch bl;
  f_case tl bl

let t_if f t1 t2 =
  check_ty_equal t1.t_ty t2.t_ty;
  t_if f t1 t2

let t_let v t1 t2 =
  check_ty_equal v.vs_ty t1.t_ty;
  t_let v t1 t2

let f_let v t1 f2 =
  check_ty_equal v.vs_ty t1.t_ty;
  f_let v t1 f2

(* generic map over types, symbols and variables *)

let rec t_gen_map fnT fnB fnV fnL t =
  let fn_t = t_gen_map fnT fnB fnV fnL in
  let fn_f = f_gen_map fnT fnB fnV fnL in
  let ty = fnT t.t_ty in
  t_label_copy t (match t.t_node with
    | Tbvar n -> t_bvar n ty
    | Tvar v -> fnV v ty
    | Tconst _ -> t
    | Tapp (f, tl) -> t_app (fnL f) (List.map fn_t tl) ty
    | Tif (f, t1, t2) -> t_if (fn_f f) (fn_t t1) (fn_t t2)
    | Tlet (t1, (u, t2)) ->
        let t1 = fn_t t1 in t_let (fnB u t1.t_ty) t1 (fn_t t2)
    | Tcase (tl, bl) ->
        let fn_b = t_branch fnT fnB fnV fnL in
        t_case (List.map fn_t tl) (List.map fn_b bl) ty
    | Teps (u, f) -> t_eps (fnB u ty) (fn_f f))

and f_gen_map fnT fnB fnV fnL f =
  let fn_t = t_gen_map fnT fnB fnV fnL in
  let fn_f = f_gen_map fnT fnB fnV fnL in
  f_label_copy f (match f.f_node with
    | Fapp (p, tl) -> f_app (fnL p) (List.map fn_t tl)
    | Fquant (q, (vl, nv, tl, f1)) ->
        let tl = tr_map fn_t fn_f tl in
        let fn_v u = fnB u (fnT u.vs_ty) in
        f_quant q (List.map fn_v vl) nv tl (fn_f f1)
    | Fbinop (op, f1, f2) -> f_binary op (fn_f f1) (fn_f f2)
    | Fnot f1 -> f_not (fn_f f1)
    | Ftrue | Ffalse -> f
    | Fif (f1, f2, f3) -> f_if (fn_f f1) (fn_f f2) (fn_f f3)
    | Flet (t, (u, f1)) ->
        let t1 = fn_t t in f_let (fnB u t1.t_ty) t1 (fn_f f1)
    | Fcase (tl, bl) ->
        let fn_b = f_branch fnT fnB fnV fnL in
        f_case (List.map fn_t tl) (List.map fn_b bl))

and t_branch fnT fnB fnV fnL (pl, nv, t) =
  (List.map (pat_s_map fnT fnB fnL) pl, nv, t_gen_map fnT fnB fnV fnL t)

and f_branch fnT fnB fnV fnL (pl, nv, f) =
  (List.map (pat_s_map fnT fnB fnL) pl, nv, f_gen_map fnT fnB fnV fnL f)

let get_fnT fn =
  let ht = Hashtbl.create 17 in
  let fnT ty =
    try Hashtbl.find ht ty.ty_tag with Not_found ->
      let nt = ty_s_map fn ty in
      Hashtbl.add ht ty.ty_tag nt;
      nt
  in
  fnT

let get_fnB () =
  let ht = Hid.create 17 in
  let fnV vs ty =
    if ty_equal vs.vs_ty ty then vs else
      try Hid.find ht vs.vs_name with Not_found ->
        let nv = create_vsymbol (id_dup vs.vs_name) ty in
        Hid.add ht vs.vs_name nv;
        nv
  in
  fnV

let get_fnV () =
  let fnB = get_fnB () in
  fun vs ty -> t_var (fnB vs ty)

let t_s_map fnT fnL t = t_gen_map (get_fnT fnT) (get_fnB ()) (get_fnV ()) fnL t
let f_s_map fnT fnL f = f_gen_map (get_fnT fnT) (get_fnB ()) (get_fnV ()) fnL f

(* simultaneous substitution into types and terms *)

let t_ty_subst mapT mapV t =
  let fnV vs _ty = try Mvs.find vs mapV with Not_found -> t_var vs in
  t_gen_map (ty_inst mapT) (get_fnB ()) fnV (fun ls -> ls) t

let f_ty_subst mapT mapV f =
  let fnV vs _ty = try Mvs.find vs mapV with Not_found -> t_var vs in
  f_gen_map (ty_inst mapT) (get_fnB ()) fnV (fun ls -> ls) f

(* fold over symbols *)

let rec t_s_fold fnT fnL acc t =
  let fn_t = t_s_fold fnT fnL in
  let fn_f = f_s_fold fnT fnL in
  let acc = ty_s_fold fnT acc t.t_ty in
  match t.t_node with
    | Tbvar _ | Tvar _ | Tconst _ -> acc
    | Tapp (f, tl) -> List.fold_left fn_t (fnL acc f) tl
    | Tif (f, t1, t2) -> fn_t (fn_t (fn_f acc f) t1) t2
    | Tlet (t1, (_,t2)) -> fn_t (fn_t acc t1) t2
    | Tcase (tl, bl) ->
        List.fold_left (t_branch fnT fnL) (List.fold_left fn_t acc tl) bl
    | Teps (_,f) -> fn_f acc f

and f_s_fold fnT fnL acc f =
  let fn_t = t_s_fold fnT fnL in
  let fn_f = f_s_fold fnT fnL in
  let fn_v acc u = ty_s_fold fnT acc u.vs_ty in
  match f.f_node with
    | Fapp (p, tl) -> List.fold_left fn_t (fnL acc p) tl
    | Fquant (_, (vl,_,tl,f1)) ->
        let acc = List.fold_left fn_v acc vl in
        fn_f (tr_fold fn_t fn_f acc tl) f1
    | Fbinop (_, f1, f2) -> fn_f (fn_f acc f1) f2
    | Fnot f1 -> fn_f acc f1
    | Ftrue | Ffalse -> acc
    | Fif (f1, f2, f3) -> fn_f (fn_f (fn_f acc f1) f2) f3
    | Flet (t, (_,f1)) -> fn_f (fn_t acc t) f1
    | Fcase (tl, bl) ->
        List.fold_left (f_branch fnT fnL) (List.fold_left fn_t acc tl) bl

and t_branch