Functorize symbolic engine

[benozol]

Fixes #116

[benozol]

We are getting closer.

These are the functor arguments for parameterizing the symbolic engine and the utllity specifications. A case_spec corresponds to the formula in a line of a table in the specifications of utilities.

colis-language/src/symbolic/symbolicUtility.mli

Lines 8 to 30 in c4497c1

	(** Definition of a symbolic filesystem to instantiate the symbolic interpreter *)
	module type FILESYSTEM = sig
	type filesystem
	end
	(** Definition of a case specification and its application to a filesystem to define
	utilities by specifications. *)
	module type CASESPEC = sig
	(** A case specification is a function from the old root variable and the new root root
	variable to a clause. *)
	type case_spec
	(** The no-op case specification introduces an equality constraint between the old root
	and the new root. *)
	val noop : case_spec
	type filesystem
	(** Apply a case specification to a filesystem, resulting in possible multiple new
	filesystems *)
	val apply_spec : filesystem -> case_spec -> filesystem list
	end

@Niols what do you think?

[Niols]

It looks good. Two questions/remarks though:

1. Why are there two types FILESYSTEM.filesystem and CASESPEC.filesystem?

2. Wouldn't that be the time to say that apply_spec only returns one filesystem, and that if your backend needs to introduce disjunctions, it should put them in the filesystem type? Basically, move the DNF situation from the engine to the backend. I am not convinced we should have made the engine aware of the fact that the constraints were always in DNF.

[benozol]

1. Why are there two types FILESYSTEM.filesystem and CASESPEC.filesystem?

FILESYSTEM and CASESPEC are arguments to different (nested) functors. Stating CASESPEC.filesystem is required to define the signature of apply_spec. FILESYSTEM and CASESPEC can be implemented by a single module of course, e.g. UtilityConstraints.{Constraints,Transducers,Mixed}

2. Wouldn't that be the time to say that apply_spec only returns one filesystem

Sure that would be possible and would enable the sharing of concrete parts of the state between the results of apply_spec. But we would have disjunctions on two levels (e.g., to implement a utility that succeeds or fails depending on the filesystem) :/ so is this "only" an optimisation issue?

[Niols]

2. Well, we already have disjunctions on two levels: the logic level and the engine+specification level. It would make sense to recover that in the code, I imagine. Also, on the constraints level, I am now designing a new system that doesn't introduce disjunctions ever. So I will always give you a singleton list. I guess transducers will also probably always give a singleton list.

[Niols]

2. Note however that it should only change from list to option, since a case spec might be impossible to apply. So this is really not so much a matter of optimisation.

[benozol]

I am now designing a new system that doesn't introduce disjunctions ever. So I will always give you a singleton list. I guess transducers will also probably always give a singleton list

In these cases there's of course no sense for apply_spec to return a list (indeed instead of an option). Should we postpone this until we #117-#125 are ready and/or the new constraint system is in place?

[Niols]

OK, let's postpone this, I'll open an issue.

[benozol]

This PR is now included in #125