prodigy.pgcl.check¶

Type Checking¶

class CheckFail(location, message)[source]¶

Bases: object

A check failed with an error message and an optional location.

Parameters:

location (Node | None)
message (str)

location: Node | None¶

message: str¶

static expected_type_got(node, expected, got)[source]¶

Parameters:

node (Node)
expected (BoolType | NatType | RealType | DistributionType)
got (BoolType | NatType | RealType | DistributionType)

Return type:

CheckFail

static expected_numeric_got(node, got)[source]¶

Parameters:

node (Node)
got (BoolType | NatType | RealType | DistributionType)

Return type:

CheckFail

static fmap(source)[source]¶

Extract an error from an iterable.

>>> CheckFail.fmap(['a'])
['a']
>>> CheckFail.fmap([CheckFail(None, 'whoops!')])
CheckFail(location=None, message='whoops!')

Parameters:: source (Iterable[_T | CheckFail])
Return type:: CheckFail | List[_T]

get_type(program, expr, check=True, predefined_functions={'bernoulli': [VarDecl(var='p', typ=RealType())], 'binomial': [VarDecl(var='n', typ=NatType(bounds=None)), VarDecl(var='p', typ=RealType())], 'geometric': [VarDecl(var='p', typ=RealType())], 'iid': [VarDecl(var='dist', typ=NatType(bounds=None)), VarDecl(var='var', typ=NatType(bounds=None))], 'logdist': [VarDecl(var='p', typ=RealType())], 'poisson': [VarDecl(var='p', typ=NatType(bounds=None))], 'sample_pgf': [VarDecl(var='dist', typ=NatType(bounds=None)), VarDecl(var='var', typ=NatType(bounds=None))], 'unif': [VarDecl(var='start', typ=NatType(bounds=None)), VarDecl(var='end', typ=NatType(bounds=None))], 'unif_d': [VarDecl(var='start', typ=NatType(bounds=None)), VarDecl(var='end', typ=NatType(bounds=None))]})[source]¶

Get the type of the expression or expectation.

Set check to True to force checking correctness of all subexpressions, even if that is not necessary to determine the given expression’s type.

>>> from .ast import *
>>> nat = NatLitExpr(10)
>>> program = Program(list(), dict(), dict(), dict(), dict(), list())

>>> get_type(program, BinopExpr(Binop.TIMES, nat, nat))
NatType(bounds=None)

>>> get_type(program, VarExpr('x'))
CheckFail(location=VarExpr('x'), message='variable is not declared')

>>> get_type(program, UnopExpr(Unop.IVERSON, BoolLitExpr(True)))
RealType()

Parameters:

program (Program)
expr (VarExpr | BoolLitExpr | NatLitExpr | RealLitExpr | UnopExpr | BinopExpr | CategoricalExpr | SubstExpr | TickExpr | FunctionCallExpr | InferExpr | SampleExpr)
predefined_functions (Dict[str, List[VarDecl]])

Return type:

BoolType | NatType | RealType | DistributionType | CheckFail

is_compatible(lhs, rhs)[source]¶

Check if the right-hand side type is compatible with the left-hand side type.

This function essentially defines the implicit type coercions of the pGCL language. Compatibility is not only important for which values can be used as the right-hand side of an assignment, but compatibility rules are also checked when operators are used.

The only rules for compatibility currently implemented are:

Natural numbers are compatible with variables of every other type of number (bounded or unbounded).
Otherwise the types must be exactly equal for values to be compatible.

>>> from .ast import Bounds

>>> is_compatible(BoolType(), BoolType())
True
>>> is_compatible(NatType(bounds=None), NatType(bounds=None))
True
>>> is_compatible(NatType(bounds=Bounds(NatLitExpr(1), NatLitExpr(5))), NatType(bounds=Bounds(NatLitExpr(1), NatLitExpr(5))))
True
>>> is_compatible(NatType(bounds=Bounds(NatLitExpr(1), NatLitExpr(5))), NatType(bounds=None))
True

>>> is_compatible(BoolType(), NatType(bounds=None))
False

Parameters:

lhs (BoolType | NatType | RealType | DistributionType)
rhs (BoolType | NatType | RealType | DistributionType)

Return type:

bool

check_instr(program, instr, predefined_functions={'bernoulli': [VarDecl(var='p', typ=RealType())], 'binomial': [VarDecl(var='n', typ=NatType(bounds=None)), VarDecl(var='p', typ=RealType())], 'geometric': [VarDecl(var='p', typ=RealType())], 'iid': [VarDecl(var='dist', typ=NatType(bounds=None)), VarDecl(var='var', typ=NatType(bounds=None))], 'logdist': [VarDecl(var='p', typ=RealType())], 'poisson': [VarDecl(var='p', typ=NatType(bounds=None))], 'sample_pgf': [VarDecl(var='dist', typ=NatType(bounds=None)), VarDecl(var='var', typ=NatType(bounds=None))], 'unif': [VarDecl(var='start', typ=NatType(bounds=None)), VarDecl(var='end', typ=NatType(bounds=None))], 'unif_d': [VarDecl(var='start', typ=NatType(bounds=None)), VarDecl(var='end', typ=NatType(bounds=None))]})[source]¶

Check a single instruction for type-safety.

>>> from .parser import parse_pgcl

>>> program = parse_pgcl("bool x; x := true")
>>> check_instr(program, program.instructions[0])

>>> program = parse_pgcl("nat x; x := true")
>>> check_instr(program, program.instructions[0])
CheckFail(location=..., message='Expected value of type NatType(bounds=None), got BoolType().')

>>> program = parse_pgcl("const x := true; x := true")
>>> check_instr(program, program.instructions[0])
CheckFail(location=..., message='x is not a variable.')

>>> program = parse_pgcl("nat x [1,5]; x := 3")
>>> check_instr(program, program.instructions[0])

>>> program = parse_pgcl("nat x [1,5]; nat y; x := x + 3")
>>> check_instr(program, program.instructions[0])

Parameters:

program (Program)
instr (SkipInstr | AbortInstr | WhileInstr | IfInstr | AsgnInstr | ChoiceInstr | LoopInstr | TickInstr | ObserveInstr | QueryInstr | ProbabilityQueryInstr | ExpectationInstr | PlotInstr | PrintInstr | OptimizationQuery)
predefined_functions (Dict[str, List[VarDecl]])

Return type:

CheckFail | None

check_program(program, predefined_functions={'bernoulli': [VarDecl(var='p', typ=RealType())], 'binomial': [VarDecl(var='n', typ=NatType(bounds=None)), VarDecl(var='p', typ=RealType())], 'geometric': [VarDecl(var='p', typ=RealType())], 'iid': [VarDecl(var='dist', typ=NatType(bounds=None)), VarDecl(var='var', typ=NatType(bounds=None))], 'logdist': [VarDecl(var='p', typ=RealType())], 'poisson': [VarDecl(var='p', typ=NatType(bounds=None))], 'sample_pgf': [VarDecl(var='dist', typ=NatType(bounds=None)), VarDecl(var='var', typ=NatType(bounds=None))], 'unif': [VarDecl(var='start', typ=NatType(bounds=None)), VarDecl(var='end', typ=NatType(bounds=None))], 'unif_d': [VarDecl(var='start', typ=NatType(bounds=None)), VarDecl(var='end', typ=NatType(bounds=None))]})[source]¶

Check a program for type-safety.

Parameters:

program (Program)
predefined_functions (Dict[str, List[VarDecl]])

Return type:

CheckFail | None

check_expression(program, expr, predefined_functions={'bernoulli': [VarDecl(var='p', typ=RealType())], 'binomial': [VarDecl(var='n', typ=NatType(bounds=None)), VarDecl(var='p', typ=RealType())], 'geometric': [VarDecl(var='p', typ=RealType())], 'iid': [VarDecl(var='dist', typ=NatType(bounds=None)), VarDecl(var='var', typ=NatType(bounds=None))], 'logdist': [VarDecl(var='p', typ=RealType())], 'poisson': [VarDecl(var='p', typ=NatType(bounds=None))], 'sample_pgf': [VarDecl(var='dist', typ=NatType(bounds=None)), VarDecl(var='var', typ=NatType(bounds=None))], 'unif': [VarDecl(var='start', typ=NatType(bounds=None)), VarDecl(var='end', typ=NatType(bounds=None))], 'unif_d': [VarDecl(var='start', typ=NatType(bounds=None)), VarDecl(var='end', typ=NatType(bounds=None))]})[source]¶

Check an expression for type-safety.

>>> program = Program(list(), dict(), dict(), dict(), dict(), list())
>>> check_expression(program, RealLitExpr("1.0"))
CheckFail(location=..., message='A program expression may not return a probability.')

Parameters:

expr (VarExpr | BoolLitExpr | NatLitExpr | RealLitExpr | UnopExpr | BinopExpr | CategoricalExpr | SubstExpr | TickExpr | FunctionCallExpr | InferExpr | SampleExpr)
predefined_functions (Dict[str, List[VarDecl]])

Return type:

CheckFail | None

check_expectation(program, expr, predefined_functions={'bernoulli': [VarDecl(var='p', typ=RealType())], 'binomial': [VarDecl(var='n', typ=NatType(bounds=None)), VarDecl(var='p', typ=RealType())], 'geometric': [VarDecl(var='p', typ=RealType())], 'iid': [VarDecl(var='dist', typ=NatType(bounds=None)), VarDecl(var='var', typ=NatType(bounds=None))], 'logdist': [VarDecl(var='p', typ=RealType())], 'poisson': [VarDecl(var='p', typ=NatType(bounds=None))], 'sample_pgf': [VarDecl(var='dist', typ=NatType(bounds=None)), VarDecl(var='var', typ=NatType(bounds=None))], 'unif': [VarDecl(var='start', typ=NatType(bounds=None)), VarDecl(var='end', typ=NatType(bounds=None))], 'unif_d': [VarDecl(var='start', typ=NatType(bounds=None)), VarDecl(var='end', typ=NatType(bounds=None))]})[source]¶

Check an expectation for type-safety.

Parameters:

expr (VarExpr | BoolLitExpr | NatLitExpr | RealLitExpr | UnopExpr | BinopExpr | CategoricalExpr | SubstExpr | TickExpr | FunctionCallExpr | InferExpr | SampleExpr)
predefined_functions (Dict[str, List[VarDecl]])

Return type:

CheckFail | None

check_function(function, context, predefined_functions={'bernoulli': [VarDecl(var='p', typ=RealType())], 'binomial': [VarDecl(var='n', typ=NatType(bounds=None)), VarDecl(var='p', typ=RealType())], 'geometric': [VarDecl(var='p', typ=RealType())], 'iid': [VarDecl(var='dist', typ=NatType(bounds=None)), VarDecl(var='var', typ=NatType(bounds=None))], 'logdist': [VarDecl(var='p', typ=RealType())], 'poisson': [VarDecl(var='p', typ=NatType(bounds=None))], 'sample_pgf': [VarDecl(var='dist', typ=NatType(bounds=None)), VarDecl(var='var', typ=NatType(bounds=None))], 'unif': [VarDecl(var='start', typ=NatType(bounds=None)), VarDecl(var='end', typ=NatType(bounds=None))], 'unif_d': [VarDecl(var='start', typ=NatType(bounds=None)), VarDecl(var='end', typ=NatType(bounds=None))]})[source]¶

Check a function for type-safety. Functions currently may only contain and return integers.

Parameters:

function (Function)
context (Program)
predefined_functions (Dict[str, List[VarDecl]])

Return type:

CheckFail | None