Taml functions:
*** Creating alphabets, variable lists, terms, rewrite rules, tree automata,
*** states, regexp (tree regular expressions), sregexp (simplified regexp).
- alphabet: (s: string) -> alphabet ---- Builds an alphabet from a string.
For example: let alpha= alphabet "f:2 g:1 a:0 b:0";;
- variables: (s: string) -> variable list ---- Builds a list of variables from a
string. For example: let vl= variables "X Y Z";;
- term: (a: alphabet) -> (v: variable list) -> (s:string) -> term ---- Builds a (ground) term from
an alphabet and a string.
For example: let t= term alpha vl "f(g(X),Y)";;
- term_list: (a: alphabet) -> (v: variable list) -> (sl:string list) ->
term list ---- Builds a list of terms from an alphabet, a list of variables
and a list of strings. For example:
let tl= term_list alpha vl ["a";"f(g(X),Y)";"f(a,a)"];;
- rule: (a:alphabet) -> (v: variable list) -> (s: string) -> rule ---- Builds a
rule on alphabet a and variable list v from a string s.
For example: let r= rule alpha vl "f(g(X),Y) -> g(X)";;
- trs: (a: alphabet) -> (v: variable list) -> (sl: string list) -> rule list
---- Builds a rule list on alphabet a and variable list v from a list of
strings. For example:
let r1= trs alpha vl ["f(g(X),Y) -> g(X)";"a -> b"];;
- automaton: (a: alphabet) -> (s: string) -> automaton ---- Builds an automaton
on alphabet a from a string s.
For example:
let a= automaton alpha "States q0 q1
Final States q0
Transitions
a -> q1
f(q0,q1) -> q0
q0 -> q1";;
- term_list_to_automaton (ts:term list) -> automaton ---- generates a tree
automaton whose recognized language is ts
- state: (i:int) -> state ---- Builds a state from its integer label.
For example: let s= state 3;;
- equation: (a:alphabet) -> (v: variable list) -> (s: string) -> equation ----
Builds an equation on alphabet a and variable list v from a string s.
For example: let e= equation alpha vl "f(g(X),Y) = f(X,Z)";;
- equation_list: (a:alphabet) -> (v: variable list) -> (sl: string list) ->
equation list ---- Builds an equation list on alphabet a and variable list
v from a list of strings sl.
For example:
let el= equation_list alpha vl ["f(g(X),Y) = g(X)";"a = b"];;
- regexp: (a: alphabet) (s: string) -> regexp ---- Builds a regexp
on alphabet a from a string s.
For example: let r1= regexp alpha "f(a, ((f(a, b) * b) . b (a)))";;
- sregexp: (a: alphabet) (s: string) -> regexp ---- Builds a **simplified**
regexp on alphabet a from a string s.
For example: let sr1= sregexp alpha "f(a,[f(a,*|a)])";;
*** Tree automata functions ****************************************************
- is_recognized: (t:term) -> (a: automaton) -> (q:state) -> bool ---- Is term
(or automaton configuration) t recognized in state q by automaton a
- filter: (tl:term list) -> (a: automaton) -> term list ---- Filters out terms
of tl that do not belong to L(a), i.e. that are not recognized by a
- gen_terms (a:automaton) -> (n:int) -> term list ---- generates the list of
terms, of maximal height n, recognized by a.
- determinise: automaton -> automaton ---- Determinisation of tree automata
- inter: (a1: automaton) -> (a2: automaton) -> automaton ---- Builds an
automaton recognizing the intersection between L(a1) and L(a2).
- union: (a1: automaton) -> (a2: automaton) -> automaton ---- Builds an
automaton recognizing L(a1) union L(a2).
- simplify: automaton -> automaton ---- Accessibility cleaning followed by
utility cleaning.
- unepsilon: (a: automaton) -> automaton ---- builds an equivalent tree
automaton without epsilon transitions, recognizing the same language. Be
careful, **unepsilon does not preserve R-compatibility.**
- inverse: (a:automaton) -> automaton ---- builds an automaton recognizing the
inverse of L(a).
- is_empty (a:automaton) -> bool ---- is the language recognized by a empty?
- is_included (a1:automaton) -> (a2:automaton) -> bool ---- is L(a1) included
in L(a2).
- is_equal (a1:automaton) -> (a2:automaton) -> bool ---- is L(a1) equal to
L(a2).
- term_list_to_automaton (ts:term list) -> automaton ---- generates a tree
automaton whose recognized language is ts
- irr: (r: rule list) -> automaton ---- Builds a tree automaton recognising the
set of terms irreducible by TRS r.
- matching: (t: term) -> (a:automaton) -> (state * substitution list) list=
matches term t on a and returns the list of couples (q,sl) where q is a state
and sl is a list of substitutions such that for all substitution s in sl,
t s -A->* q.
- add_trans (a:automaton) -> (lt: transition list) -> automaton ---- adds
transitions lt to tree automaton a
- merge (a:automaton) (ml: (state * state) list): automaton ---- merges all
pairs of states of ml in the tree automaton a
- automaton_to_string (a:automaton) -> string ---- produces the pretty printed
string of automaton a
- automaton_alphabet (a:automaton) -> alphabet ---- alphabet associated to a
given tree automaton
*** Tree Automata Completion functions *****************************************
- timbuk_completion (i:int) -> (a:automaton) -> (trs: rule list) ->
(eq: equation list) -> (pl: term list) -> (verbose:bool) ->
(automaton * bool * (term * state * substitution list) list)
timbuk's completion: performs a maximum of i completion steps with trs and
simplification with eq and checks if a term of pl list is reachable. In the
result, the 'automaton' is the completed automaton, the 'bool' is true if the
automaton is complete (R-compatible), the '(term * state * substitution list)
list' is the list of all substitutions found when matching terms of pl on the
completed tree automaton. If this list is empty, no pattern of pl is reachable.
- timbuk_fun_completion (i:int) -> (a:automaton) -> (atc: automaton) ->
(trs: rule list) -> (pl: term list) -> (equation list * automaton * bool)
timbuk's completion for functional TRS: performs a maximum of i completion
steps with trs. trs is supposed to be terminating and sufficiently complete
(i.e. all rewriting derivation eventually leads to a well typed term of T(C).
Simplication equations are automatically generated from the automaton atc
which recognizes well typed constructor terms of T(C). The set of equation is
generated so that terms of pl should not be reachable (equations are
automatically built and refined). In the result, the 'equation list' is the
list of automatically generated equations to achieve a terminating completion,
the 'automaton' is the completed automaton, the 'bool' is true if the
automaton is complete (R-compatible).
*** Term functions *************************************************************
- apply: (s:substitution) -> (t:term) -> term ---- applies substitution s on
term t
- normalize_term (t: term) -> (a:automaton) -> (q:state): transition list ----
gives the necessary transitions to add to a for term t to be recognized in
state q
*** Substitution functions *****************************************************
- apply: (s:substitution) -> (t:term) -> term ---- applies substitution s on
term t
- value: (s:substitution) -> (v:variable) -> state option ---- If s is a state
substitution, returns the value Some(q) if the state associated to v in s is
q, and None otherwise
- domain: (s:substitution) -> variable list ---- the domain of a substitution
*** Rewrite Rules functions ****************************************************
- lhs: (r: rule) -> term ---- Gets the left-hand side of a rewrite rule
- rhs: (r: rule) -> term ---- Gets the right-hand side of a rewrite rule
- conditions: (r: rule) -> conditions list ---- Gets the condition list of a
rewrite rule (if any)
- rule_alphabet (r:rule) -> alphabet ---- alphabet associated to a given
rewrite rule
*** Equation accessors *********************************************************
- elhs: (r: equation) -> term ---- Gets the left-hand side of an equation
- erhs: (r: equation) -> term ---- Gets the right-hand side of an equation
*** Regular expressions functions **********************************************
- regexp_to_automaton (r:regexp) -> automaton ---- builds a tree automaton from
the regular expression r
- sregexp_to_automaton (sr:sregexp) -> automaton ---- builds a tree automaton
from the simplified regular expression sr
- sregexp_to_regexp (sr:sregexp) -> regexp ---- converts a simplified regular
sr expression to a regular expression
- automaton_to_regexp (aut:automaton) -> regexp ---- converts an automaton aut
to a regular expression
- automaton_to_sregexp (aut:automaton) -> sregexp ---- converts an automaton to
a **simplified** regular expression if this is possible. Otherwise a
ConversionFailure exception is raised
- regexp_alphabet (r:regexp) -> alphabet ---- alphabet associated to a given
regexp
- sregexp_alphabet (s:sregexp) -> alphabet ---- alphabet associated to a given
sregexp
*** The help function **********************************************************
- help: unit -> unit ---- Prints this help message