Dcalc.AutotestThis module scans a program for "test" scopes, detected as scopes without any undefined inputs. It runs the interpreter to compute their results, then inserts assertion in the code that ensure correctness of said results.
val scope :
Shared_ast.decl_ctx ->
Catala_utils.Global.backend_lang ->
((Shared_ast.dcalc, 'm) Shared_ast.gexpr Shared_ast.boxed ->
(Shared_ast.dcalc, 'm) Shared_ast.gexpr Shared_ast.boxed) ->
Shared_ast.ScopeName.t ->
(Shared_ast.dcalc, 'm) Shared_ast.gexpr Shared_ast.scope_body ->
(Shared_ast.dcalc, 'm) Shared_ast.gexpr Shared_ast.scope_body Bindlib.boxIf the given scope has any inputs, does nothing but reboxing. Otherwise, this function runs the interpreter on the scope to determine its outputs, then inserts assertions within the scope.
NOTE: scopes with context variables are *not* treated at the moment ; functional values are ignored in the equality assertions
val program : 'm Ast.program -> 'm Ast.program