Functorize Symbolic Engine

[Niols]

As a first step towards plugging a transducer backend into the symbolic engine, we need to factorize the latter. I think the only thing the engine need are an abstract type for a filesystem (or a transformation of filesystem, the engine doesn't have to know the difference) and a dispatch function.

---

The Why3 code seems to be quite a lot constraints-aware:

colis-language/src/symbolic/driver.drv

Lines 1 to 6 in a4da8ec

	module symbolicInterpreter.Constraints
	syntax type clause "Colis_constraints.Clause.sat_conj"
	syntax type variable "Colis_constraints.Var.t"
	syntax type feature "Colis_constraints.Feat.t"
	syntax type path "Colis_constraints.Path.t"
	end

But I think this is only used to define the type for a filesystem. And that type should probably be abstract for the symbolic engine, and defined in the constraint backend only?

colis-language/src/symbolic/symbolicInterpreter.mlw

Lines 24 to 28 in a4da8ec

	type filesystem = {
	root : variable;
	clause : clause;
	root0 : option variable;
	}

---

The pathes from constraints are also used in Why3. Do we really need that? We could either provide a generic "path" notion, not included in the constraints. We could even only use strings, maybe? I don't know. It should go out of the constraints anyway.

colis-language/src/symbolic/driver.drv

Lines 11 to 12 in a4da8ec

	syntax val absolute_or_concat_relative "Colis_constraints.Path.(normalize ~cwd:%1 (from_string %2))"
	syntax val normalized_path_to_string "Colis_constraints.Path.normal_to_string %1"

---

I think the only other function needed would be the dispatch function, under a form or an other.

colis-language/src/symbolic/driver.drv

Lines 18 to 20 in a4da8ec

	module symbolicInterpreter.Interpreter
	syntax val sym_interp_utility "BatSet.to_list (SymbolicUtility.dispatch' %1 %2 %3)"
	end

colis-language/src/symbolic/symbolicInterpreter.mlw

Line 324 in a4da8ec

val function sym_interp_utility (ctx:utility_context) (id:identifier) (sta:state) : Cn.t (state, bool)

[Niols]

(While I'm at it, what is that?)

colis-language/src/symbolic/driver.drv

Line 10 in a4da8ec

syntax val interp_utility "assert false"

[Niols]

I think this is the right place to cut and functorize. It also shows in the code the actual separation and gives us for free these tracing "monad transformers" we talked about.

However, as you note in your e-mail, this will force the people from WP2 to reimplement quite a lot of things. Which is why I was talking during the meeting about an other functor, taking a more detailed interface to the backend as argument – including maybe this famous under_specification function that hides constraint-specific stuff – and providing basically the type and the dispatch function for the other functor.

This would allow to really cut into three parts:

• the symbolic engine, very backend agnostic,
• the dispatch function, including a lot of machinery and concrete execution, rather backend agnostic but showing why we need composition of transducers/logic formulas,
• the backend and specifications themselves.

wdyt?

[benozol]

IIUC you propose three functors to generalize the filesystem: 1) one for the symbolic engine, 2) one for the toplevel dispatch function, and 3) one that abstracts away the FS in under_specifications.

That’s certainly possible, but restrict code abstraction only to a level that is actually required I want to point out two issues about putting the dispatch function in the functorizebale interface:

1. Your motivation for monad transformers on the toplevel is clean tracing. Tracing, however, should either happen on the level of language instructions, or on the level of specification cases (as it currently is the case). Tracing on the toplevel dispatch of utilities offers less information than the two alternatives.

2. Since Sylvain et al. plan to follow the symbolic specifications of utilities for the transducers specifications, they should use the functorization under_specifications instead of a toplevel dispatch functor. We should instead investigate how to extend the symbolic formalizations of specifications by transducers (by either adding a field for transducers in SymbolicUtility.case or parameterizing field spec)

But—alas!—by functorizing symbolic engine and under specifications we probably have to functorize the dispatch part :)

More remarks:

But I think this is only used to define the type for a filesystem. And that type should probably be abstract for the symbolic engine, and defined in the constraint backend only?

Yes that is the functorization of the symbolic engine

The pathes from constraints are also used in Why3. Do we really need that?

Paths and features have to be compatible with what is used in the constraint engine. But they are actually very concrete and should be shared with the transducers engine. Yes, outsourcing them from the constraints lib sounds right.

While I'm at it, what is that? assert false

The function interp_utility is defined in the concrete semantics. In the symbolic engine it is only used to specify sym_interp_utility and never executed (and this driver file is only used for extracting the symbolic interpreter)

[Niols]

So I think I only suggest on functor: The one that abstracts the backend of the symbolic engine, asking basically just for a constraint type and a dispatch function that takes the current constraint, the simple command to run and returns a list of constraints tagged by success or error. I think that is what we agreed on with the people from WP2?

And then I make the remark (that I think you make also) that it would be a shame to code the whole dispatch function in all backends, especially because most "interesting" (that is except maybe dummy ones, or a tracing backend, etc.) backends will look the same: a generic dispatch function calling a specifications data bank and combining them using a logical "thing" (very specific, I know!). So I suggest a second functor here. Basically a helper to build backends suitable for the first functor.

I think your remark is valid and it's not possible to only functorise the second without the first one anyway. But even if it is, I don't think it's a good idea. I find the first functor very satisfying because it shows how the work has been very cleanly split between symbolic engine and constraints backend.

And then, about tracing, it is not a motivation or a goal, I was just saying that it would come for free with the first functor. I agree with the fact that tracing at the level of specifications has more information, but it relies on implementers to provide the correct tracing and make that information available. Tracing at the level of dispatch would still have the calling context, the exact command call and the returned cases with their success/error tags, which is nearly as much as what is currently printed anyway. It would then remove the burden of tracing from the specifications and provide a consistent trace in the output. Besides, by being very localised in just one module somewhere, it would become very easy to change the way we trace, what we print, or what we keep, etc. etc. But again, I believe this should not be a goal, but it comes for free with the first functor so we can think about it when functorisation is done!

I hope I was clearer this time?

[benozol]

Solved by #125