Previous  Up  

Module Apron.Parser

module Parser: sig .. end

Introduction

This small module implements the parsing of expressions, constraints and generators. The allowed syntax is simple for linear expressions (no parenthesis) but supports interval expressions. The syntax is more flexible for tree expressions.

Syntax

lincons ::= linexpr ('>' | '>=' | '=' | '!=' | '=' | '<=' | '<') linexpr | linexpr = linexpr 'mod' scalar

gen ::= ('V:' | 'R:' | 'L:' | 'RM:' | 'LM:') linexpr

linexpr ::= linexpr '+' linterm | linexpr '-' linterm | linterm

linterm ::= coeff ['*'] identifier | coeff | ['-'] identifier

tcons ::= texpr ('>' | '>=' | '=' | '!=' | '=' | '<=' | '<') texpr | texpr = texpr 'mod' scalar

texpr ::= coeff | identifier | unop texpr | texpr binop texpr | '(' texpr ')'

binop ::= ('+'|'-'|'*'|'/'|'%')['_'('i'|'f'|'d'|'l'|'q')][','('n'|'0'|'+oo'|'-oo')]

unop ::= ('cast' | 'sqrt')['_'('i'|'f'|'d'|'l'|'q')][','('n'|'0'|'+oo'|'-oo')]

coeff ::= scalar | ['-'] '['scalar ';' scalar ']'

scalar ::= ['-'] (integer | rational | floating_point_number)

For tree expressions texpr, by default the operations have an exact arithmetic semantics in the real numbers (even if involved variables are of integer). The type qualifiers modify this default semantics. Their meaning is as follows:

By default, the rounding mode is "any" (this applies only in non-real semantics), which allows to emulate all the following rounding modes:

Examples

let (linexpr:Linexpr1.t) = Parser.linexpr1_of_string env "z+0.4x+2y"

let (tab:Lincons1.earray) = Parser.lincons1_of_lstring env ["1/2x+2/3y=1";"[1;2]<=z+2w";"z+2w<=4";"0<=u";"u<=5"]

let (generator:Generator1.t) = Parser.generator1_of_string env "R:x+2y"

let (texpr:Texpr1.t) = Parser.texpr1_of_string env "a %_i,? b +_f,0 c"

Remarks

There is the possibility to parse directly from a lexing buffer, or from a string (from which one can generate a buffer with the function Lexing.from_string.

This module uses the underlying modules Apron_lexer and Apron_parser.

Interface


exception Error of string
Raised by conversion functions
val linexpr1_of_lexbuf : Apron.Environment.t -> Lexing.lexbuf -> Apron.Linexpr1.t
val lincons1_of_lexbuf : Apron.Environment.t -> Lexing.lexbuf -> Apron.Lincons1.t
val generator1_of_lexbuf : Apron.Environment.t -> Lexing.lexbuf -> Apron.Generator1.t
Conversion from lexing buffers to resp. linear expressions, linear constraints and generators, defined on the given environment.
val texpr1expr_of_lexbuf : Lexing.lexbuf -> Apron.Texpr1.expr
val texpr1_of_lexbuf : Apron.Environment.t -> Lexing.lexbuf -> Apron.Texpr1.t
val tcons1_of_lexbuf : Apron.Environment.t -> Lexing.lexbuf -> Apron.Tcons1.t
Conversion from lexing buffers to resp. tree expressions and constraints, defined on the given environment.
val linexpr1_of_string : Apron.Environment.t -> string -> Apron.Linexpr1.t
val lincons1_of_string : Apron.Environment.t -> string -> Apron.Lincons1.t
val generator1_of_string : Apron.Environment.t -> string -> Apron.Generator1.t
Conversion from strings to resp. linear expressions, linear constraints and generators, defined on the given environment.
val texpr1expr_of_string : string -> Apron.Texpr1.expr
val texpr1_of_string : Apron.Environment.t -> string -> Apron.Texpr1.t
val tcons1_of_string : Apron.Environment.t -> string -> Apron.Tcons1.t
Conversion from lexing buffers to resp. tree expressions and constraints, defined on the given environment.
val lincons1_of_lstring : Apron.Environment.t -> string list -> Apron.Lincons1.earray
val generator1_of_lstring : Apron.Environment.t -> string list -> Apron.Generator1.earray
Conversion from lists of strings to array of resp. linear constraints and generators, defined on the given environment.
val tcons1_of_lstring : Apron.Environment.t -> string list -> Apron.Tcons1.earray
Conversion from lists of strings to array of tree constraints.
val of_lstring : 'a Apron.Manager.t ->
       Apron.Environment.t -> string list -> 'a Apron.Abstract1.t
Abstraction of lists of strings representing constraints to abstract values, on the abstract domain defined by the given manager.