package catala
Install
Dune Dependency
Authors
Maintainers
Sources
md5=6dbbc2f50c23693f26ab6f048e78172f
sha512=a5701e14932d8a866e2aa3731f76df85ff2a68b4fa943fd510c535913573274d66eaec1ae6fcae17f20b475876048a9ab196ef6d8c23d4ea6b90b986aa0a6daa
doc/catala.scopelang/Scopelang/Ast/index.html
Module Scopelang.Ast
Source
Abstract syntax tree of the scope language
Identifiers
module StructFieldMapLift : sig ... end
module EnumConstructorMapLift : sig ... end
type location =
| ScopeVar of ScopeVar.t Utils.Marked.pos
| SubScopeVar of ScopeName.t * SubScopeName.t Utils.Marked.pos * ScopeVar.t Utils.Marked.pos
Abstract syntax tree
type typ =
| TLit of Dcalc.Ast.typ_lit
| TStruct of StructName.t
| TEnum of EnumName.t
| TArrow of typ Utils.Marked.pos * typ Utils.Marked.pos
| TArray of typ
| TAny
The expressions use the Bindlib library, based on higher-order abstract syntax
and expr =
| ELocation of location
| EVar of expr Bindlib.var
| EStruct of StructName.t * marked_expr StructFieldMap.t
| EStructAccess of marked_expr * StructFieldName.t * StructName.t
| EEnumInj of marked_expr * EnumConstructor.t * EnumName.t
| EMatch of marked_expr * EnumName.t * marked_expr EnumConstructorMap.t
| ELit of Dcalc.Ast.lit
| EAbs of (expr, marked_expr) Bindlib.mbinder * typ Utils.Marked.pos list
| EApp of marked_expr * marked_expr list
| EOp of Dcalc.Ast.operator
| EDefault of marked_expr list * marked_expr * marked_expr
| EIfThenElse of marked_expr * marked_expr * marked_expr
| EArray of marked_expr list
| ErrorOnEmpty of marked_expr
type io_input =
| NoInput
(*For an internal variable defined only in the scope, and does not appear in the input.
*)| OnlyInput
(*For variables that should not be redefined in the scope, because they appear in the input.
*)| Reentrant
(*For variables defined in the scope that can also be redefined by the caller as they appear in the input.
*)
This type characterizes the three levels of visibility for a given scope variable with regards to the scope's input and possible redefinitions inside the scope..
type io = {
io_output : bool Utils.Marked.pos;
(*
*)true
is present in the output of the scope.io_input : io_input Utils.Marked.pos;
}
Characterization of the input/output status of a scope variable.
type rule =
| Definition of location Utils.Marked.pos * typ Utils.Marked.pos * io * expr Utils.Marked.pos
| Assertion of expr Utils.Marked.pos
| Call of ScopeName.t * SubScopeName.t
type scope_decl = {
scope_decl_name : ScopeName.t;
scope_sig : (typ Utils.Marked.pos * io) ScopeVarMap.t;
scope_decl_rules : rule list;
}
type program = {
program_scopes : scope_decl ScopeMap.t;
program_enums : enum_ctx;
program_structs : struct_ctx;
}
Variable helpers
val make_abs :
vars ->
expr Utils.Marked.pos Bindlib.box ->
typ Utils.Marked.pos list ->
Utils.Pos.t ->
expr Utils.Marked.pos Bindlib.box
val make_app :
expr Utils.Marked.pos Bindlib.box ->
expr Utils.Marked.pos Bindlib.box list ->
Utils.Pos.t ->
expr Utils.Marked.pos Bindlib.box
val make_let_in :
Var.t ->
typ Utils.Marked.pos ->
expr Utils.Marked.pos Bindlib.box ->
expr Utils.Marked.pos Bindlib.box ->
expr Utils.Marked.pos Bindlib.box
val make_default :
?pos:Utils.Pos.t ->
expr Utils.Marked.pos list ->
expr Utils.Marked.pos ->
expr Utils.Marked.pos ->
expr Utils.Marked.pos
make_default ?pos exceptions just cons
builds a term semantically equivalent to <exceptions | just :- cons>
(the EDefault
constructor) while avoiding redundant nested constructions. The position is extracted from just
by default.
Note that, due to the simplifications taking place, the result might not be of the form EDefault
:
<true :- x>
is rewritten asx
<ex | true :- def>
, whendef
is a default term<j :- c>
without exceptions, is collapsed into<ex | def>
<ex | false :- _>
, whenex
is a single exception, is rewritten asex