Module Desugared.AstSource

Abstract syntax tree of the desugared representation

Names, Maps and Keys

Sourcemodule IdentMap : Map.S with type key = String.t
Sourcemodule RuleMap : Map.S with type key = RuleName.t
Sourcemodule RuleSet : Set.S with type elt = RuleName.t
Sourcemodule LabelMap : Map.S with type key = LabelName.t
Sourcemodule LabelSet : Set.S with type elt = LabelName.t
Sourcemodule ScopeVarSet : Set.S with type elt = ScopeVar.t
Sourcemodule ScopeVarMap : Map.S with type key = ScopeVar.t
Sourcemodule ScopeDef : sig ... end

Inside a scope, a definition can refer either to a scope def, or a subscope def

Sourcemodule ScopeDefMap : Map.S with type key = ScopeDef.t
Sourcemodule ScopeDefSet : Set.S with type elt = ScopeDef.t

AST

Expressions

The expressions use the Bindlib library, based on higher-order abstract syntax

Variable helpers

Sourcemodule Var : sig ... end
Sourcemodule VarMap : Map.S with type key = Var.t
Sourcetype vars = expr Bindlib.mvar
Sourceval make_var : Var.t Utils.Pos.marked -> expr Utils.Pos.marked Bindlib.box
Sourceval make_app : expr Utils.Pos.marked Bindlib.box -> expr Utils.Pos.marked Bindlib.box list -> Utils.Pos.t -> expr Utils.Pos.marked Bindlib.box
Sourceval make_let_in : Var.t -> Scopelang.Ast.typ Utils.Pos.marked -> expr Utils.Pos.marked Bindlib.box -> expr Utils.Pos.marked Bindlib.box -> expr Utils.Pos.marked Bindlib.box

Rules and scopes

Sourcetype rule = {
  1. rule_id : RuleName.t;
  2. rule_just : expr Utils.Pos.marked Bindlib.box;
  3. rule_cons : expr Utils.Pos.marked Bindlib.box;
  4. rule_parameter : (Var.t * Scopelang.Ast.typ Utils.Pos.marked) option;
  5. rule_exception_to_rules : RuleSet.t Utils.Pos.marked;
}
Sourceval always_false_rule : Utils.Pos.t -> Scopelang.Ast.typ Utils.Pos.marked option -> rule
Sourcetype assertion = expr Utils.Pos.marked Bindlib.box
Sourcetype variation_typ =
  1. | Increasing
  2. | Decreasing
Sourcetype reference_typ =
  1. | Decree
  2. | Law
Sourcetype meta_assertion =
  1. | FixedBy of reference_typ Utils.Pos.marked
  2. | VariesWith of unit * variation_typ Utils.Pos.marked option
Sourcetype scope_def = {
  1. scope_def_rules : rule RuleMap.t;
  2. scope_def_typ : Scopelang.Ast.typ Utils.Pos.marked;
  3. scope_def_is_condition : bool;
  4. scope_def_io : Scopelang.Ast.io;
  5. scope_def_label_groups : RuleSet.t LabelMap.t;
}
Sourcetype var_or_states =
  1. | WholeVar
  2. | States of StateName.t list
Sourcetype scope = {
  1. scope_vars : var_or_states ScopeVarMap.t;
  2. scope_sub_scopes : Scopelang.Ast.ScopeName.t Scopelang.Ast.SubScopeMap.t;
  3. scope_uid : Scopelang.Ast.ScopeName.t;
  4. scope_defs : scope_def ScopeDefMap.t;
  5. scope_assertions : assertion list;
  6. scope_meta_assertions : meta_assertion list;
}
Sourcetype program = {
  1. program_scopes : scope Scopelang.Ast.ScopeMap.t;
  2. program_enums : Scopelang.Ast.enum_ctx;
  3. program_structs : Scopelang.Ast.struct_ctx;
}

Helpers

Sourceval locations_used : expr Utils.Pos.marked -> LocationSet.t