This module provides functions that are overloaded for different term classes. Term class is denoted with an explicit instance of type ('a,'b)cls, where 'a stands for the parent term and 'b for the child term.
Example
Give a block
# let b = Blk.create ();;
val b : Blk.t =
00000003:
We can append a definition to it with an overloaded Term.append
clone term creates an object with a fresh new identifier that has the same contents as term, i.e., that is syntactically the same. The clone operation is shallow, all subterms of term are unchanged.
remove t p id returns a term that doesn't contain element with the a given id
val change :
('a, 'b)cls->'at->tid->('bt option->'bt option)->'at
change t p id f if p contains subterm with of a given kind t and identifier id, then apply f to this subterm. Otherwise, apply f to None. If f return None, then remove this subterm (a given it did exist), otherwise, update parent with a new subterm.
map t p ~f returns term p with all subterms of type t mapped with function f
val filter_map : ('a, 'b)cls->'at->f:('bt->'bt option)->'at
filter_map t p ~f returns term p with all subterms of type t filter_mapped with function f, i.e., all terms for which function f returned Some thing are substituted by the thing, otherwise they're removed from the parent term
val concat_map : ('a, 'b)cls->'at->f:('bt->'bt list)->'at
concat_map t p ~f substitute subterm c of type t in parent term p with f c. If f c is an empty list, then c doesn't occur in a new parent term, if f c is a singleton list, then c is substituted with the f c, like in map. If f c is a list of n elements, then in the place of c this n elements are inserted.
val filter : ('a, 'b)cls->'at->f:('bt-> bool)->'at
filter t p ~f returns a term p with subterms c for which f c = false removed.
prev t p id returns a term that preceeds a term with a given id, if such exists.
val after : ('a, 'b)cls->?rev:bool ->'at->tid->'btseq
after t ?rev p tid returns all subterms in term p that occur after a term with a given tid. if rev is true or omitted then terms are returned in the evaluation order. Otherwise they're reversed. If there is no term with a given tid, then an empty sequence is returned.
val before : ('a, 'b)cls->?rev:bool ->'at->tid->'btseq
before t ?rev p tid returns all term that occurs before defintion with a given tid in blk. If there is no such definition, then the sequence will be empty.
val append : ('a, 'b)cls->?after:tid->'at->'bt->'at
append t ~after:this p c returns the p term with c appended after this term. If after is not specified, then append def to the end of the parent term (if it makes sense, otherwise it is just added). If this doesn't occur in the p term then do nothing. The term tid is preserved.
val prepend : ('a, 'b)cls->?before:tid->'at->'bt->'at
prepend t ~before:this p c returns the p with c inserted before this term. If before is left unspecified, then insert the c at the beginning of the p if it is a sequence, otherwise just insert. If this is specified but doesn't occur in the p then p is returned as is. In all cases, the returned term has the same tid as p.
nth_exn t p n same as nth, but raises exception if n is not a valid position number.
Attributes
Terms attribute set can be extended, using universal values. A value of type 'a tag is used to denote an attribute of type 'a with the name Value.Tag.name tag.
With the provided interface Term can be treated as an extensible record.
Mapper perfoms deep identity term mapping. If you override any method make sure that you didn't forget to invoke parent's method, as OCaml will not call it for you.
Visitor performs deep visiting. As always, don't forget to overrid parent methods. The visitor comes with useful enter_Tleave_T that are no-ops in this visitor, so if you inherit directly from it, then you may not call to the parent method.
switch cls t ~program ~sub .. ~jmp performs a pattern matching over a term t based on its type class cls. It is guaranteed that only one function will be called for a term.