pGCL grammar¶

The Lark grammar that prodigy.pgcl.parser is built from. Expressions are parsed with the operator table of prodigy.pgcl.util.lark_expr_parser, which is appended as the rule expression.

start: declarations instructions queries

    declarations: declaration* -> declarations

    declaration: "bool" var                  -> bool
               | "real" var bounds?          -> real
               | "const" var ":=" expression -> const
               | "rparam" var                -> rparam
               | "nparam" var                -> nparam
               | "fun" var ":=" function     -> fun
               | "nat" var bounds?           -> nat
               | "dist" var                  -> dist

    bounds: "[" expression "," expression "]"

    function: "{" declarations instructions "return" rvalue "}"

    instructions: instruction* -> instructions

    queries: query* -> queries

    instruction: "skip"                                      -> skip
               | "abort"                                     -> abort
               | "while" "(" expression ")" block            -> while
               | "if" "(" expression ")" block "else"? block -> if
               | var ":=" rvalue                             -> assign
               | block "[" expression "]" block              -> choice
               | "tick" "(" expression ")"                   -> tick
               | "observe" "(" expression ")"                -> observe
               | "loop" "(" INT ")" block                    -> loop
               | "query" "{" instructions "}"                -> query

    query: "?Ex" "[" expression "]"                          -> expectation
               | "?Pr" "[" expression "]"                    -> prquery
               | "!Print"                                    -> print
               | "!Plot" "[" var ("," var)? ("," literal)?"]"-> plot
               | "?Opt" "[" expression "," var "," var "]"   -> optimize


    block: "{" instruction* "}"

    rvalue: expression
          | "infer" "{" function_call "}" -> infer
          | "sample" "{" var "}"          -> sample

    function_call: var "(" parameter_list? ")"

    parameter_list: positional_params "," named_params 
                  | positional_params 
                  | named_params

    positional_params: positional_param
                     | positional_params "," positional_param

    positional_param: rvalue

    named_params: named_param 
                | named_params "," named_param

    named_param: var ":=" rvalue

    literal: "true"  -> true
           | "false" -> false
           | INT     -> nat
           | FLOAT   -> real
           | "∞"     -> infinity
           | "\infty" -> infinity

    var: CNAME


    %ignore /#.*$/m
    %ignore /\/\/.*$/m
    %ignore WS
    %ignore ";"

    %import common.CNAME
    %import common.INT
    %import common.FLOAT
    %import common.WS

    ?expression: expression_0
    ?expression_0: expression_1
        | expression_0 "||" expression_1 -> or
    ?expression_1: expression_2
        | expression_1 "&" expression_2 -> and
    ?expression_2: expression_3
        | expression_2 "<=" expression_3 -> leq
        | expression_2 "<" expression_3 -> le
        | expression_2 ">" expression_3 -> ge
        | expression_2 ">=" expression_3 -> geq
        | expression_2 "=" expression_3 -> eq
    ?expression_3: expression_4
        | "-" expression_3 -> uminus
    ?expression_4: expression_5
        | expression_4 "+" expression_5 -> plus
        | expression_4 "-" expression_5 -> minus
    ?expression_5: expression_6
        | expression_5 ":" expression_6 -> likely
    ?expression_6: expression_7
        | expression_6 "*" expression_7 -> times
        | expression_6 "/" expression_7 -> divide
        | expression_6 "%" expression_7 -> mod
    ?expression_7: expression_8
        | expression_8 "^" expression_7 -> power
    ?expression_8: "not " expression_8 -> neg
        | "(" expression ")" -> parens
        | "[" expression "]" -> iverson
        | literal -> literal
        | var -> var
        | function_call -> function_call

Division¶

/ is rational division everywhere; it never rounds. Floor division (//) does not exist yet; it is planned in #105.

In a guard, x/2 <= 1 means x <= 2, not floor(x/2) <= 1 (which would also hold for x = 3).
An assignment to a nat variable requires the result to be a natural number in every state, e.g. x := x/2 only where x is always even. Otherwise the update is rejected; it is never rounded.

Guards¶

Comparisons in guards (if, while, observe) are compared over the rationals. Guards with one variable can be filtered on every distribution, including infinite ones; other guards need a variable with a finite marginal. Linear guards are first rewritten exactly into guards with natural numbers only:

Exact normalisation of linear guards (normalize_guard()).

A comparison whose sides are built from variables, constants, +, multiplication by a constant and division by a constant is linear. It is compared exactly over the rationals, e.g. 1/2*x < 2 holds if and only if x < 4. As everywhere, / is rational division, so x/2 <= 1 means x <= 2 and not floor division. The comparison is rewritten into an equivalent guard with natural numbers only:

with one variable it becomes x < n, x <= n, x = n, x > n or x >= n for a natural number n, or true or false (x = 3/2 never holds), which every engine can filter even on infinite distributions;
with several variables and a constant that is not a natural number or a division, both sides are multiplied by the least common denominator, e.g. 1/2*x + 1/3*y < 1 becomes 3*x + 2*y < 6;
without variables it becomes true or false.

Subtraction is not linear here, as x - y on natural numbers is truncated at 0 by some engines. A guard with a constant that is not a natural number but that is not linear (e.g. x*y < 1/2 or x % 2 = 1/2) is rejected on every engine, as its value depends on how an engine treats non-natural intermediate results.

LinearForm

A linear combination of variables; the key “” holds the constant.

alias of Dict[str, Fraction]

normalize_guard(condition, variables)[source]

An equivalent guard with natural numbers only if condition is a linear comparison (see the module documentation), or None if there is nothing to normalise.

Raises a ValueError if condition is a comparison with a constant that is not a natural number but not linear.

Parameters:

condition (VarExpr | BoolLitExpr | NatLitExpr | RealLitExpr | UnopExpr | BinopExpr | CategoricalExpr | SubstExpr | TickExpr | FunctionCallExpr | InferExpr | SampleExpr)
variables (Set[str])

Return type: