Module Subs


module Subs: sig .. end

Substitutions



type subs 
val empty : subs
Identity: substitution with no binding
val is_empty : subs -> bool
Test if a substitution is the identity
val subs : Var.var -> Term.term -> subs
One-variable substitution
val add : Var.var -> Term.term -> subs -> subs
Add a new binding: replace the previous one if any
val check_add : Var.var -> Term.term -> subs -> subs
Add to s the mapping (x,t) if mem s x = false or find s x = t. raise Failure otherwise
val find : Var.var -> subs -> Term.term
Raise Not_found if var is not bound
val mem : Var.var -> subs -> bool
Test if there is a binding
val map : (Term.term -> Term.term) -> subs -> subs
Map a function on bindings
val apply : subs -> Term.term -> Term.term
Apply a substitution to a term
val domain : subs -> Var.VarSet.t
Domain of a substitution
val restrict : subs -> Var.VarSet.t -> subs
Restriction of a susbtitution to some domain
val comp : subs -> subs -> subs
Composition of 2 substitutions: apply (comp s1 s2) t = apply s1 (apply s2 t)
val comp_res : subs -> subs -> subs
Restricted composition: comp_res s1 s2 = restrict (domain s2) (comp s1 s2)
val inverse : subs -> subs
Inverse a substitution mapping variables to variables. Raise Failure otherwise
val fprintf : Format.formatter -> subs -> unit
Print a substitution into a formatter.