Module Logic.ExpandSource

This module implements the expand algorithm of Makoto Kanazawa's article "Parsing and generation as Datalog query evaluation" to deal with almost linear grammars.

Log is the log module for Expand

Sourcemodule Address : sig ... end

The Address module implements addresses as used in Makoto's paper

Sourcemodule AddSet : sig ... end

The AddSet module implements a trie data structure to represent sets of Address.t addresses

collapse ~consts t returns None if t is unchanged through the collapse algorithm (i.e., no subterm of atomic type occurs at least twice in t), and Some u where u is the results of the (recursive) collapse algorithm.

It is expected that t does not contain unexpanded defined constants.

If consts is provided, the mapping from constant ids to strings (in some signature) is used to pretty prints terms if Log log level is set to some adequate level. Otherwise, each constant is printed as Const[i].