congress.datalog.compile module

class congress.datalog.compile.Compiler

Bases: object

Process Congress policy file.

print_parse_result()
raise_errors()
read_source(input, input_string=False, theories=None, use_modules=True)
sigerr(error)
sigwarn(error)
class congress.datalog.compile.DatalogSyntax(theories=None, use_modules=True)

Bases: object

Read Datalog syntax and convert it to internal representation.

class Lexer(char_stream, state=None)

Bases: congress.datalog.Python3.CongressLexer.CongressLexer

displayRecognitionError(token_names, e)
getErrorHeader(e)

What is the error header, normally line/character position information?

class Parser(tokens, state=None)

Bases: congress.datalog.Python3.CongressParser.CongressParser

displayRecognitionError(token_names, e)
getErrorHeader(e)

What is the error header, normally line/character position information?

antlr_atom_str(antlr)
atom_vars(antlr_atom)
convert_to_congress(antlr)
create(antlr)
create_and_literals(antlr)
create_atom_aux(antlr)
create_atom_dual_arg_list(antlr)

Get parameter list and named list

Return (i) a list of compile.Term representing the positionally specified parameters in the ANTLR atom and (ii) a dictionary mapping string/number to compile.Term representing the name/index-specified parameters. If there are errors self.errors is modified.

create_event(antlr)
create_literal(antlr)
create_modal_atom(antlr)
create_rule(antlr)
create_tablename(antlr)
create_term(antlr)
literal_and_vars(antlr_and)
classmethod parse_file(input, input_string=False)
rule_variables(antlr_rule)

Get variables in the rule.

Returns a set of all variable names (as strings) that occur in the given rule ANTLR_RULE.

unused_variable_prefix(antlr_rule)

Get unused variable prefix.

Returns variable prefix (string) that is used by no other variable in the rule ANTLR_RULE.

variable_name(antlr)
class congress.datalog.compile.Event(formula=None, insert=True, proofs=None, target=None)

Bases: object

Represents a change to a formula.

formula
insert
is_insert()
lstr()
proofs
tablename(default_theory=None)
target
class congress.datalog.compile.Fact(table, values)

Bases: tuple

Represent a Fact (a ground literal)

Use this class to represent a fact such as Foo(1,2,3). While one could use a Rule to represent the same fact, this Fact datastructure is more memory efficient than a Rule object since this Fact stores the information as a native tuple, containing native values like ints and strings. Notes that this subclasses from tuple.

SORT_RANK = 3
class congress.datalog.compile.Literal(table, arguments, location=None, negated=False, use_modules=True, id_=None, name=None, comment=None, original_str=None, named_arguments=None)

Bases: object

Represents a possibly negated atomic statement, e.g. p(a, 17, b).

SORT_RANK = 5
argument_names()

Return names of all arguments. Ignores named_arguments.

arguments
comment
complement()

Copies SELF and inverts is_negated.

classmethod create_from_iter(list)

Create Literal from list.

LIST is a python list representing an atom, e.g. [‘p’, 17, “string”, 3.14]. Returns the corresponding Literal.

classmethod create_from_table_tuple(table, tuple)

Create Literal from table and tuple.

TABLE is a string tablename. TUPLE is a python list representing a row, e.g. [17, “string”, 3.14]. Returns the corresponding Literal.

drop_theory()

Destructively sets the theory to None.

drop_update()
eliminate_column_references_and_pad_positional(theories, default_theory=None, index=0, prefix='')

Expand column references to positional args and pad positional args.

Expand column references to traditional datalog positional args. Also pad positional args if too few are provided. Returns a new literal. If no column reference, unless no schema found for the table.

id
invert_update()
is_atom()
is_builtin(check_arguments=True)
is_ground()

Return True if all args are non-vars. Ignores named_arguments.

is_negated()
is_rule()
is_update()
location
make_positive()

Return handle to self or copy of self based on positive check.

Either returns SELF if is_negated() is false or returns copy of SELF where is_negated() is set to false.

make_update(is_insert=True)
name
named_arguments
negated
original_str
plug(binding, caller=None)

Assumes domain of BINDING is Terms. Ignores named_arguments.

pretty_str()
set_comment(comment)
set_id(id)
set_name(name)
set_original_str(original_str)
table
tablename(default_service=None)
theory_name()
variable_names()

Return variable names in arguments. Ignores named_arguments.

variables()

Return variables in arguments. Ignores named_arguments.

class congress.datalog.compile.ObjectConstant(name, type, location=None)

Bases: congress.datalog.compile.Term

Represents a term with a fixed value.

FLOAT = 'FLOAT'
INTEGER = 'INTEGER'
SORT_RANK = 2
STRING = 'STRING'
is_object()
is_variable()
location
name
type
class congress.datalog.compile.Rule(head, body, location=None, id=None, name=None, comment=None, original_str=None)

Bases: object

Represents a rule, e.g. p(x) :- q(x).

SORT_RANK = 6
body
comment
drop_theory()

Destructively sets the theory to None in all heads.

drop_update()
eliminate_column_references_and_pad_positional(theories, default_theory=None)

Return version of SELF /w col refs removed and pos args padded.

All column references removed. Positional args padded up to required length. Throws exception if RULE is inconsistent with schemas.

head
heads
id
invert_update()
is_atom()
is_rule()
is_update()
location
make_update(is_insert=True)
name
original_str
plug(binding, caller=None)
plug_body(binding, caller=None)
plug_heads(binding, caller=None)
pretty_str()
set_comment(comment)
set_id(id)
set_name(name)
set_original_str(original_str)
tablename(theory=None)
tablenames(theory=None, body_only=False, include_builtin=False, include_modal=True)

Return all the tablenames occurring in this rule.

theory_name()
variable_names()
variables()
class congress.datalog.compile.RuleDependencyGraph(formulas=None, theory=None, include_atoms=True, select_head=None, select_body=None, head_to_body=True)

Bases: congress.datalog.utility.BagGraph

A Graph representing the table dependencies of rules.

Creates a Graph that includes one node for each table and an edge <u,v> if there is some rule with u in the head and v in the body. THEORY is the name of the theory to be used for any literal whose theory is None. INCLUDE_ATOMS is a boolean controlling whether atoms should contribute to nodes. SELECT_HEAD is a function that returns True for those head literals that should be included in the graph. SELECT_BODY is a function that returns True for those body literals that should be included in the graph. HEAD_TO_BODY controls whether edges are oriented from the tables in the head toward the tables in the body, or vice versa.

find_definitions(tables)
find_dependencies(tables)
formula_delete(formula, theory=None, include_atoms=True, select_head=None, select_body=None)

Delete rows/edges for the given FORMULA.

formula_insert(formula, theory=None, include_atoms=True, select_head=None, select_body=None)

Insert rows/edges for the given FORMULA.

formula_nodes_edges(formula, theory=None, include_atoms=True, select_head=None, select_body=None)

Compute dependency graph nodes and edges for FORMULA.

Returns (NODES, EDGES, MODALS), where NODES/EDGES are sets and MODALS is a ModalIndex. Each EDGE is a tuple of the form (source, destination, label).

formula_update(events, include_atoms=True, select_head=None, select_body=None)

Modify graph with inserts/deletes in EVENTS.

Returns list of changes.

table_delete(table)
tables()
tables_with_modal(modal)
undo_changes(changes)

Reverse the given changes.

Each change is either (‘node’, <node>, <is-insert>) or (‘edge’, <src_node>, <dst_node>, <label>, <is_insert>) or (‘modal’, <modal-index>, <is-insert>).

class congress.datalog.compile.Schema(dictionary=None, complete=False)

Bases: object

Meta-data about a collection of tables.

arity(tablename)

Returns the number of columns for the given TABLENAME.

Return None if TABLENAME is unknown.

column_name(tablename, column)

Returns name for given COLUMN or None if it is unknown.

column_number(tablename, column)

Returns the 0-indexed position of the given COLUMN for TABLENAME.

Returns None if TABLENAME or COLUMNNAME are unknown. Returns COLUMN if it is a number.

columns(tablename)

Returns the list of column names for the given TABLENAME.

Return None if the tablename’s columns are unknown.

revert(change)

Revert change made by update.

Return None

types(tablename)

Returns the list of column names for the given TABLENAME.

Return None if the tablename’s columns are unknown.

update(item, is_insert)

Returns the schema change of this update.

Return schema change.

class congress.datalog.compile.Tablename(table=None, service=None, modal=None)

Bases: object

SORT_RANK = 4
classmethod build_service_table(service, table)

Return string service:table.

classmethod create_from_tablename(tablename, service=None, use_modules=True)
drop_service()
drop_update()

Drop the update.

If end of table name is + or -, return a copy without the sign. If table name does not end in + or -, make no copy.

global_tablename(prefix=None)
invert_update()

Invert the update.

If end of table name is + or -, return a copy after switching the copy’s sign. Does not make a copy if table name does not end in + or -.

is_update()
make_update(is_insert=True)

Turn the tablename into a +/- update.

matches(service, table, modal)
modal
name(default_service=None)

Compute string name with default service.

classmethod parse_service_table(tablename)

Given tablename returns (service, name).

same(other, default_service)

Equality but where default_service is used for None service.

service
table
class congress.datalog.compile.Term

Bases: object

Represents the union of Variable and ObjectConstant.

Should only be instantiated via factory method.

static create_from_python(value, force_var=False)

Create Variable or ObjectConstants.

To create variable, FORCE_VAR needs to be true. There is currently no way to avoid this since variables are strings.

class congress.datalog.compile.Variable(name, location=None)

Bases: congress.datalog.compile.Term

Represents a term without a fixed value.

SORT_RANK = 1
is_object()
is_variable()
location
name
congress.datalog.compile.check_schema_consistency(item, theories, theory=None)
congress.datalog.compile.fact_errors(atom, theories=None, theory=None)

Checks if ATOM has any errors.

THEORIES is a dictionary mapping a theory name to a theory object.

congress.datalog.compile.fact_has_no_theory(atom)

Checks that ATOM has an empty theory. Returns exceptions.

congress.datalog.compile.find_subpolicy(rules, required_tables, prohibited_tables, output_tables)

Return a subset of rules pertinent to the parameters.

Param

rules is the collection of Datalog rules to analyze

Param

required_tables is the set of tablenames that a rule must depend on

Param

prohibited_tables is the set of tablenames that a rule must NOT depend on.

Param

output_tables is the set of tablenames that all rules must support.

Table R depends on table T if T occurs in the body of a rule with R in the head, or T occurs in the body of a rule where R depends on the table in the head of that rule.

The subset of RULES chosen has several properties:

  1. if a chosen rule has table R in the head, then one of @output_tables depends on R

  2. if a chosen rule has R in the head, then R does not depend on any of @prohibited_tables

  3. if a chosen rule has R in the head, then R depends on at least

    one of @required_tables.

congress.datalog.compile.formulas_to_string(formulas)

Convert formulas to string.

Takes an iterable of compiler sentence objects and returns a string representing that iterable, which the compiler will parse into the original iterable.

congress.datalog.compile.get_compiler(args, theories=None, use_modules=True)

Run compiler as per ARGS and return the compiler object.

congress.datalog.compile.is_atom(x)

Returns True if object X is an atomic Datalog formula.

congress.datalog.compile.is_atom_like(x)
congress.datalog.compile.is_atom_rule(x)
congress.datalog.compile.is_datalog(x)

Returns True if X is an atom or a rule with one head.

congress.datalog.compile.is_extended_datalog(x)

Returns True if X is a valid datalog sentence.

Allows X to be a multi_rule in addition to IS_DATALOG().

congress.datalog.compile.is_literal(x)

Check if x is Literal.

Returns True if X is a possibly negated atomic Datalog formula and one that if replaced by an ATOM syntactically be replaced by an ATOM.

congress.datalog.compile.is_literal_like(x)
congress.datalog.compile.is_literal_rule(x)
congress.datalog.compile.is_multi_rule(x)

Returns True if X is a rule with multiple heads.

congress.datalog.compile.is_recursive(x)

Check for recursive.

X can be either a Graph or a list of rules. Returns T iff the list of rules RULES has a table defined in Terms of itself.

congress.datalog.compile.is_regular_rule(x)

Returns True if X is a rule with a single head.

congress.datalog.compile.is_result(x)

Check if x is result representation.

Returns T iff x is a formula or tablename representing the result of an action invocation.

congress.datalog.compile.is_rule(x)

Returns True if x is a rule.

congress.datalog.compile.is_stratified(rules)

Check if rules are stratified.

Returns T iff the list of rules RULES has no table defined in terms of its negated self.

congress.datalog.compile.is_update(x)

Returns T iff x is a formula or tablename representing an update.

congress.datalog.compile.keywords_safety(lit)
congress.datalog.compile.literal_schema(literal, theories, default_theory=None, theory_assertion=None)

Return the schema that applies to LITERAL or None.

Param

LITERAL is a Literal for which we want the schema

Param

THEORIES is a dictionary mapping the name of the theory to the theory object

Param

DEFAULT_THEORY is the theory to use if no theory is recorded as part of LITERAL

Returns

the schema that applies to LITERAL or None

congress.datalog.compile.literal_schema_consistency(literal, theories, theory=None)

Returns list of errors, but does no checking if column references.

congress.datalog.compile.literal_theory(literal, theories, default_theory=None)

Return the theory that applies to LITERAL or None.

Param

LITERAL is a Literal for which we want the schema

Param

THEORIES is a dictionary mapping the name of the theory to the theory object

Param

DEFAULT_THEORY is the theory to use if no theory is recorded as part of LITERAL

Returns

the theory that applies to LITERAL or None

congress.datalog.compile.parse(policy_string, theories=None, use_modules=True)

Run compiler on policy string and return the parsed formulas.

congress.datalog.compile.parse1(policy_string, theories=None, use_modules=True)

Run compiler on policy string and return 1st parsed formula.

congress.datalog.compile.parse_file(filename, theories=None)

Compile the file.

Run compiler on policy stored in FILENAME and return the parsed formulas.

congress.datalog.compile.print_antlr(tree)

Print an antlr Tree.

congress.datalog.compile.print_tree(tree, text, kids, ind=0)

Helper function for printing.

Print out TREE using function TEXT to extract node description and function KIDS to compute the children of a given node. IND is a number representing the indentation level.

congress.datalog.compile.reorder_for_safety(rule)

Reorder the rule.

Moves builtins/negative literals so that when left-to-right evaluation is performed all of a builtin’s inputs are bound by the time that builtin is evaluated. Reordering is stable, meaning that if the rule is properly ordered, no changes are made.

congress.datalog.compile.rule_body_safety(rule)

Check rule body for safety.

Checks if every variable in a negative literal also appears in a positive literal in the body. Checks if every variable in a builtin input appears in the body. Returns list of exceptions.

congress.datalog.compile.rule_errors(rule, theories=None, theory=None)

Returns list of errors for RULE.

congress.datalog.compile.rule_head_has_no_theory(rule, permit_head=None)

Checks if head of rule has None for theory. Returns exceptions.

PERMIT_HEAD is a function that takes a literal as argument and returns True if the literal is allowed to have a theory in the head.

congress.datalog.compile.rule_head_safety(rule)

Checks if every variable in the head of RULE is also in the body.

Returns list of exceptions.

congress.datalog.compile.rule_modal_safety(rule)

Check if the rule obeys the restrictions on modals.

congress.datalog.compile.rule_schema_consistency(rule, theories, theory=None)

Returns list of problems with rule’s schema.

congress.datalog.compile.schema_consistency(thing, theories, theory=None)
congress.datalog.compile.stratification(rules)

Stratify the rules.

Returns a dictionary from table names to an integer representing the strata to which the table is assigned or None if the rules are not stratified.

congress.datalog.compile.string_is_servicename(name)

Returns True if @name can be a servicename in the policy language.