The 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.Python2.CongressLexer.CongressLexer
-
displayRecognitionError
(token_names, e)¶
-
getErrorHeader
(e)¶
-
-
class
Parser
(tokens, state=None)¶ Bases:
congress.datalog.Python2.CongressParser.CongressParser
-
displayRecognitionError
(token_names, e)¶
-
getErrorHeader
(e)¶
-
-
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
-
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.
-
classmethod
col
(cols)¶
-
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
-
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.
-
static
-
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: i) if a chosen rule has table R in the head, then one of @output_tables
depends on R- if a chosen rule has R in the head, then R does not depend on any of @prohibited_tables
- 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.