package catala

  1. Overview
  2. Docs
package catala
Legend:
Library
Module
Module type
Parameter
Class
Class type

This file makes explicit few structural invariants of the dcalc asbtract syntax tree. Those invariants have been checked on all tests and examples of catala. The behavior of the compiler on programs that don't follow those invariant in undefined.

val check_all_invariants : Shared_ast.typed Ast.program -> bool

Check all invariants. Return true if all the invariants are correct. Print errors messages for each unsucessfull invariants. Here are all the invariants checked:

  • invariant_default_no_arrow check no default term has a function type.
  • invariant_no_partial_evaluation check there is no partial function.
  • invariant_no_return_a_function check no function return a function.
  • invariant_app_inversion : if the term is an function application, then there is only 6 possibility : it is a let binding, it is an operator application, it is an variable application, it is a struct access function application (sub-scope call), it is a operator application with trace, or an external function.
  • invariant_match_inversion : if a term is a match, then every branch is an function abstraction.
  • invariant_typing_default: the type TDefault can only appear in some positions.

The function prints as a side effect the different errors.