package catala

You can search for identifiers within the package.

in-package search v0.2.0

package catala

The Catala compiler
- Compiler utilities
- Default calculus
- Desugared representation
- Lambda calculus
- Literate programming
- Example backend plugins
- Statement calculus
- The scope language
- Default calculus
- Catala surface representation
- Verification
- Library api_web
  - Api_web
    
    D
    
    To_jsoo
- Library catala.catala_utils
  - Catala_utils
    
    Cli
    
    Flags
    
    Global
    
    File
    
    Set
    
    Map
    
    Tree
    
    Global
    
    Map
    
    OrderedType
    
    S
    
    Make
    
    Mark
    
    marked_map
    
    marked_iter
    
    pos_map
    
    pos_iter
    
    Message
    
    Content
    
    Pos
    
    String
    
    Set
    
    Map
    
    Suggestions
    
    Uid
    
    Info
    
    MarkedString
    
    Id
    
    Set
    
    Map
    
    Style
    
    Make
    
    Set
    
    Map
    
    Gen
    
    Set
    
    Map
    
    Module
    
    Set
    
    Map
    
    Path
    
    Gen_qualified
    
    Set
    
    Map
    
    Version
- Library catala.clerk_driver
  - Clerk_driver
- Library catala.dcalc
  - Dcalc
    
    Ast
    
    From_scopelang
    
    Invariants
- Library catala.desugared
  - Desugared
    
    Ast
    
    ScopeDef
    
    Map
    
    Set
    
    AssertionName
    
    Set
    
    Map
    
    LocationSet
    
    ExprMap
    
    Rule
    
    Dependency
    
    Vertex
    
    Edge
    
    ScopeDependencies
    
    V
    
    E
    
    EdgeExceptions
    
    ExceptionVertex
    
    ExceptionsDependencies
    
    V
    
    E
    
    Disambiguate
    
    From_surface
    
    Linting
    
    Name_resolution
    
    Print
- Library catala.driver
  - Driver
    
    Passes
    
    Commands
    
    Plugin
- Library catala.lcalc
  - Lcalc
    
    Ast
    
    Closure_conversion
    
    Compile_with_exceptions
    
    Compile_without_exceptions
    
    From_dcalc
    
    Monomorphize
    
    To_ocaml
- Library catala.literate
  - Literate
    
    Html
    
    Latex
    
    Literate_common
    
    Pygment_lexers
    
    Internal
    
    Pygmentize
- Library catala.runtime_jsoo
  - Runtime_jsoo
    
    Runtime
    
    source_position
    
    raw_event
    
    event
    
    event_manager
    
    duration
- Library catala.runtime_ocaml
  - Runtime_ocaml
    
    Runtime
    
    Eoption
    
    EventParser
    
    Json
    
    Oper
- Library catala.scalc
  - Scalc
    
    Ast
    
    D
    
    L
    
    FuncName
    
    Set
    
    Map
    
    VarName
    
    Set
    
    Map
    
    From_lcalc
    
    Print
    
    To_c
    
    To_python
    
    To_r
- Library catala.scopelang
  - Scopelang
    
    Ast
    
    LocationSet
    
    Dependency
    
    SDependencies
    
    V
    
    E
    
    TVertex
    
    TVertexSet
    
    TDependencies
    
    V
    
    E
    
    From_desugared
    
    Print
- Library catala.shared_ast
  - Shared_ast
    
    Runtime
    
    ModuleName
    
    ScopeName
    
    Set
    
    Map
    
    TopdefName
    
    Set
    
    Map
    
    StructName
    
    Set
    
    Map
    
    StructField
    
    Set
    
    Map
    
    EnumName
    
    Set
    
    Map
    
    EnumConstructor
    
    Set
    
    Map
    
    RuleName
    
    Set
    
    Map
    
    LabelName
    
    Set
    
    Map
    
    Ident
    
    ScopeVar
    
    Set
    
    Map
    
    StateName
    
    Set
    
    Map
    
    Op
    
    Var
    
    Set
    
    Map
    
    Qident
    
    Set
    
    Map
    
    Type
    
    Map
    
    Operator
    
    Expr
    
    Box
    
    BoundList
    
    Scope
    
    Program
    
    Print
    
    EXPR_PARAM
    
    ExprGen
    
    ExprConciseParam
    
    ExprDebugParam
    
    UserFacing
    
    Typing
    
    Env
    
    Interpreter
    
    Optimizations
- Library catala.surface
  - Surface
    
    Ast
    
    map
    
    Fill_positions
    
    Lexer_common
    
    LocalisedLexer
    
    Lexer_en
    
    Lexer_fr
    
    Lexer_pl
    
    Parser
    
    Make
    
    MenhirInterpreter
    
    Incremental
    
    Parser_driver
    
    Parser_errors
    
    Print
    
    Tokens
- Library catala.verification
  - Verification
    
    Conditions
    
    Globals
    
    Io
    
    Backend
    
    BackendIO
    
    MakeBackendIO
    
    Solver
    
    Z3backend
    
    Io
- Library explain
  - Explain
    
    Env
    
    V
    
    E
    
    G
    
    V
    
    E
    
    GTopo
- Library json_schema
  - Json_schema
    
    D
    
    To_json
- Library lazy_interpreter
  - Lazy_interpreter
    
    Lazy_interp
    
    Env
- Library python
  - Python
- Sources
  - api_web
    
    api_web.ml
  - catala.catala_utils
    
    catala_utils.ml
    
    cli.ml
    
    file.ml
    
    global.ml
    
    map.ml
    
    mark.ml
    
    message.ml
    
    pos.ml
    
    string.ml
    
    suggestions.ml
    
    uid.ml
    
    version.ml
  - catala.clerk_driver
    
    clerk_driver.ml
    
    clerk_driver__.ml
    
    clerk_runtest.ml
    
    clerk_scan.ml
  - catala.dcalc
    
    ast.ml
    
    dcalc.ml
    
    from_scopelang.ml
    
    invariants.ml
  - catala.desugared
    
    ast.ml
    
    dependency.ml
    
    desugared.ml
    
    disambiguate.ml
    
    from_surface.ml
    
    linting.ml
    
    name_resolution.ml
    
    print.ml
  - catala.driver
    
    driver.ml
    
    driver__.ml
    
    plugin.ml
  - catala.lcalc
    
    ast.ml
    
    closure_conversion.ml
    
    compile_with_exceptions.ml
    
    compile_without_exceptions.ml
    
    from_dcalc.ml
    
    lcalc.ml
    
    monomorphize.ml
    
    to_ocaml.ml
  - catala.literate
    
    html.ml
    
    latex.ml
    
    literate.ml
    
    literate_common.ml
    
    pygment_lexers.ml
    
    pygmentize.ml
  - catala.runtime_jsoo
    
    runtime.ml
    
    runtime_jsoo.ml
  - catala.runtime_ocaml
    
    runtime.ml
    
    runtime_ocaml.ml
  - catala.scalc
    
    ast.ml
    
    from_lcalc.ml
    
    print.ml
    
    scalc.ml
    
    to_c.ml
    
    to_python.ml
    
    to_r.ml
  - catala.scopelang
    
    ast.ml
    
    dependency.ml
    
    from_desugared.ml
    
    print.ml
    
    scopelang.ml
  - catala.shared_ast
    
    boundList.ml
    
    definitions.ml
    
    expr.ml
    
    interpreter.ml
    
    operator.ml
    
    optimizations.ml
    
    print.ml
    
    program.ml
    
    qident.ml
    
    scope.ml
    
    shared_ast.ml
    
    shared_ast__.ml
    
    type.ml
    
    typing.ml
    
    var.ml
  - catala.surface
    
    ast.ml
    
    fill_positions.ml
    
    lexer_common.ml
    
    lexer_en.ml
    
    lexer_fr.ml
    
    lexer_pl.ml
    
    parser.ml
    
    parser_driver.ml
    
    parser_errors.ml
    
    print.ml
    
    surface.ml
    
    tokens.ml
  - catala.verification
    
    conditions.ml
    
    globals.ml
    
    io.ml
    
    solver.ml
    
    verification.ml
    
    z3backend.ml
  - explain
    
    explain.ml
  - json_schema
    
    json_schema.ml
  - lazy_interpreter
    
    lazy_interp.ml
    
    lazy_interpreter.ml
  - python
    
    python.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Z3backend.Io`Source

Sourceval init_backend : unit -> unit

Sourcetype backend_context

Sourceval make_context : Shared_ast.decl_ctx -> backend_context

Sourcetype vc_encoding

Source

val translate_expr : 
  backend_context ->
  Shared_ast.typed Dcalc.Ast.expr ->
  backend_context * vc_encoding

Source

val encode_asserts : 
  backend_context ->
  Shared_ast.typed Dcalc.Ast.expr ->
  backend_context

Sourcetype model

Sourcetype vc_encoding_result =

| Success of vc_encoding * backend_context
| Fail of string

Source

val print_negative_result : 
  Conditions.verification_condition ->
  backend_context ->
  model option ->
  string

Source

val encode_and_check_vc : 
  Shared_ast.decl_ctx ->
  (Conditions.verification_condition * vc_encoding_result) ->
  bool

encode_and_check_vc spawns a new Z3 solver and tries to solve the expression vc. Returns true if the vs was proven true and false otherwise. *

package catala

Module Z3backend.IoSource

Module `Z3backend.Io`Source