The following file is just a scratchpad, and can be ignored.

<!-- Draft README.md 
# Usage

## Parsing Formulas
Consider the string representation of a logical formula (in infix notation, e.g., "p∧q" or in function notation, e.g. "∧(p,q)". Such expressions can easily be parsed to a `SyntaxTree` representation using the method `parsebaseformula`. As you can see from the documentation, it is highly customizable, allowing parsing custom-defined operators and changing how recognized propositions must be interpreted (e.g. in "true∧false" propositions are booleans, while in "1∧0" they are integers).


The `SyntaxTree` returned by `parsebaseformula` can be paired with a logic (a grammar and an algebra) using `parsebaseformula`, thus returning a Formula: the latter method disposes of the same flexibility of `parsetree` TODO not true.

## Generating random formulas
Random formulas generation is provided by the following methods:
- randformula (which returns a SyntaxTree);
- randbaseformula (which returns a SyntaxTree anchored to a Logic, thus, a Formula).

Both allow customizing the generation process by setting an alphabet (that is, which propositional letters are in play), an operators vector, the maximum height of the SyntaxTree and the maximum modal depth (that is, the maximum number of modal operators, if any, in each SyntaxTree path).

Notes for Giovanni; 
1) many important definitions are introduced here: is this the correct place to explain them or it's better to just link the documentation? 
2) I'm still working on putting a modal_depth parameter in both randbaseformula and randformula 
3) As stated in AbstractSyntaxStructure docstring, classically a logical formula is implemented using a tree structure (an AST) but other representations may exist: I guess we could add a "randnormalform" method

## Generating random interpretations
Kripke structures generation is provided by gen_kstructure interface. As you can see from the documentation, internally it builds up a random directed graph structure (using some, possibly custom algorithm). The adjacency list obtained is enriched with informations to obtain a so called Kripke frame; this is done by taking each vertex in the list and

- converting it into a World structure;
- defining which worlds are accessible from this following a specific relation (I'm trying to summarize both the concept of binary accessiblity relation R and the accessibles method...).

Finally, pairing each world in the Kripke frame with a list of propositional letters (this goes undeer the name of world valuation function), a Kripke structure is returned by gen_kstructure.

## Model checking

## Interpretation sets

 -->

-------------------------------------------------------------------------------------------

syntaxstring:

DONE: 0) clone, instantiate and checkout in dev-v0.9.1 the following packages: SoleBase, SoleData.

DONE: 1) rename parentheses in parentheses, and parenthesis in paranthesis.

2) make syntaxstring more readable (by default, not all parentheses are displayed.)
	2.1) optional parameter "allparentheses"
	2.2) testing both with allparantheses=false (default) and true)

DONE: 3) propositional-logic:
	julia> t2 = TruthDict(["a" => true, "b" => false, "c" => true, "d" => false, "e" => true, "f" => true])
	TruthDict wrapping:
	Dict{Proposition{String}, Bool} with 3 entries:
		Proposition{String}("c") => 1
		Proposition{String}("b") => 0
		Proposition{String}("a") => 1

	* rename TruthDict in TruthDict
	then, change 

	function Base.show(
		io::IO,
		i::TruthDict{A,T,D},
	) where {A,T<:TruthValue,D<:AbstractDict{<:Proposition{<:A},T}}
		# println(io, "TruthDict{$(A),$(T),$(D)} wrapping:")
		println(io, "TruthDict wrapping:")
		Base.display(i.truth)
	end

4) Read SoleData documentation
	4.1) Eventually, make a custom branch

##### JUL 17

# TODO establish the trait is_right_associative (defaulted to false, but true for implication)
#		look at operator associativity table (in C). 
#		fix parsing accordingly

# TODO in syntaxstring, parameter remove_redundant_parentheses (with examples)