Module Mlang.Mir

type cat_computed =
| Base
| GivenBack
module CatCompSet : SetExt.T with type elt = cat_computed
type cat_variable =
| CatInput of StrSet.t
| CatComputed of CatCompSet.t
val pp_cat_variable : Stdlib.Format.formatter -> cat_variable -> unit
val compare_cat_variable : cat_variable -> cat_variable -> int
module CatVarSet : SetExt.T with type elt = cat_variable
module CatVarMap : MapExt.T with type key = cat_variable
type cat_variable_loc =
| LocCalculated
| LocBase
| LocInput
type cat_variable_data = {
id : cat_variable;
id_str : string;
id_int : int;
loc : cat_variable_loc;
pos : Pos.t;
attributs : Pos.t StrMap.t;
}
type variable_id = int

Each variable has an unique ID

type variable = {
name : string Pos.marked;(*

The position is the variable declaration

*)
alias : string option;(*

Input variable have an alias

*)
id : variable_id;
descr : string Pos.marked;(*

Description taken from the variable declaration

*)
attributes : Mast.variable_attribute list;
origin : variable option;(*

If the variable is an SSA duplication, refers to the original (declared) variable

*)
cats : cat_variable option;
is_table : int option;
is_temp : bool;
is_it : bool;
}
type local_variable = {
id : int;
}
type typ =
| Real

Type of MIR values

type literal =
| Float of float
| Undefined
type func =
| SumFunc(*

Sums the arguments

*)
| AbsFunc(*

Absolute value

*)
| MinFunc(*

Minimum of a list of values

*)
| MaxFunc(*

Maximum of a list of values

*)
| GtzFunc(*

Greater than zero (strict) ?

*)
| GtezFunc(*

Greater or equal than zero ?

*)
| NullFunc(*

Equal to zero ?

*)
| ArrFunc(*

Round to nearest integer

*)
| InfFunc(*

Truncate to integer

*)
| PresentFunc(*

Different than zero ?

*)
| Multimax(*

???

*)
| Supzero(*

???

*)
| VerifNumber
| ComplNumber

MIR only supports a restricted set of functions

MIR expressions are simpler than M; there are no loops or syntaxtic sugars.

Because translating to MIR requires a lot of unrolling and expansion, we introduce a LocalLet construct to avoid code duplication.

type 'variable expression_ =
| Unop of Mast.unop * 'variable expression_ Pos.marked
| Comparison of Mast.comp_op Pos.marked * 'variable expression_ Pos.marked * 'variable expression_ Pos.marked
| Binop of Mast.binop Pos.marked * 'variable expression_ Pos.marked * 'variable expression_ Pos.marked
| Index of 'variable Pos.marked * 'variable expression_ Pos.marked
| Conditional of 'variable expression_ Pos.marked * 'variable expression_ Pos.marked * 'variable expression_ Pos.marked
| FunctionCall of func * 'variable expression_ Pos.marked list
| Literal of literal
| Var of 'variable
| LocalVar of local_variable
| LocalLet of local_variable * 'variable expression_ Pos.marked * 'variable expression_ Pos.marked
| NbCategory of CatVarSet.t
| Attribut of string Pos.marked * 'variable * string Pos.marked
| Size of 'variable
| NbAnomalies
| NbDiscordances
| NbInformatives
| NbBloquantes
type expression = variable expression_
module VariableMap : MapExt.T with type key = variable

MIR programs are just mapping from variables to their definitions, and make a massive use of VariableMap.

module VariableDict : Dict.S with type key = variable_id and type elt = variable
module VariableSet : SetExt.T with type elt = variable
module LocalVariableMap : sig ... end
type 'variable index_def =
| IndexTable of 'variable expression_ Pos.marked IndexMap.t
| IndexGeneric of 'variable * 'variable expression_ Pos.marked
type 'variable variable_def_ =
| SimpleVar of 'variable expression_ Pos.marked
| TableVar of int * 'variable index_def
| InputVar
type variable_def = variable variable_def_
type 'variable variable_data_ = {
var_definition : 'variable variable_def_;
var_typ : typ option;(*

The typing info here comes from the variable declaration in the source program

*)
}
type variable_data = variable variable_data_
type rov_id =
| RuleID of int
| VerifID of int
module RuleMap : MapExt.T with type key = rov_id
type 'a domain = {
dom_id : Mast.DomainId.t Pos.marked;
dom_names : Pos.t Mast.DomainIdMap.t;
dom_by_default : bool;
dom_min : Mast.DomainIdSet.t;
dom_max : Mast.DomainIdSet.t;
dom_rov : IntSet.t;
dom_data : 'a;
dom_used : int Pos.marked option;
}
type rule_domain_data = {
rdom_computable : bool;
}
type rule_domain = rule_domain_data domain
type 'variable print_arg =
| PrintString of string
| PrintName of string Pos.marked * variable
| PrintAlias of string Pos.marked * variable
| PrintIndent of 'variable expression_ Pos.marked
| PrintExpr of 'variable expression_ Pos.marked * int * int
type error_descr = {
kind : string Pos.marked;
major_code : string Pos.marked;
minor_code : string Pos.marked;
description : string Pos.marked;
isisf : string Pos.marked;
}

Errors are first-class objects

type error = {
name : string Pos.marked;(*

The position is the variable declaration

*)
id : int;(*

Each variable has an unique ID

*)
descr : error_descr;(*

Description taken from the variable declaration

*)
typ : Mast.error_typ;
}
module Error : sig ... end
type instruction =
| Affectation of variable_id * variable_data
| IfThenElse of expression * instruction Pos.marked list * instruction Pos.marked list
| ComputeTarget of string Pos.marked
| VerifBlock of instruction Pos.marked list
| Print of Mast.print_std * variable print_arg Pos.marked list
| Iterate of variable_id * CatVarSet.t * expression Pos.marked * instruction Pos.marked list
| Restore of Pos.t VariableMap.t * (variable * CatVarSet.t * expression Pos.marked) list * instruction Pos.marked list
| RaiseError of error * string option
| CleanErrors
| ExportErrors
| FinalizeErrors
type rule_data = {
rule_apps : Pos.t StrMap.t;
rule_domain : rule_domain;
rule_chain : (string * rule_domain) option;
rule_vars : instruction Pos.marked list;
rule_number : rov_id Pos.marked;
}
type target_data = {
target_name : string Pos.marked;
target_file : string option;
target_apps : string Pos.marked list;
target_tmp_vars : (variable * Pos.t * int option) StrMap.t;
target_prog : instruction Pos.marked list;
}
type verif_domain_data = {
vdom_auth : CatVarSet.t;
vdom_verifiable : bool;
}
type verif_domain = verif_domain_data domain
type 'variable condition_data_ = {
cond_seq_id : int;
cond_number : rov_id Pos.marked;
cond_domain : verif_domain;
cond_expr : 'variable expression_ Pos.marked;
cond_error : error * 'variable option;
cond_cats : int CatVarMap.t;
}
type condition_data = variable condition_data_

We translate string variables into first-class unique Mir.variable, so we need to keep a mapping between the two. A name is mapped to a list of variables because variables can be redefined in different rules

type program = {
program_safe_prefix : string;
program_applications : Pos.t StrMap.t;
program_var_categories : cat_variable_data CatVarMap.t;
program_rule_domains : rule_domain Mast.DomainIdMap.t;
program_verif_domains : verif_domain Mast.DomainIdMap.t;
program_chainings : rule_domain Mast.ChainingMap.t;
program_vars : VariableDict.t;(*

A static register of all variables that can be used during a calculation

*)
program_targets : target_data TargetMap.t;
program_idmap : idmap;
}
module Variable : sig ... end
module LocalVariable : sig ... end

Local variables don't appear in the M source program but can be introduced by let bindings when translating to MIR. They should be De Bruijn indices but instead are unique globals identifiers out of laziness.

val false_literal : literal
val true_literal : literal
val num_of_rule_or_verif_id : rov_id -> int
val find_var_name_by_alias : program -> string Pos.marked -> string
val map_expr_var : ( 'v -> 'v2 ) -> 'v expression_ -> 'v2 expression_
val fold_expr_var : ( 'a -> 'v -> 'a ) -> 'a -> 'v expression_ -> 'a
val map_var_def_var : ( 'v -> 'v2 ) -> 'v variable_def_ -> 'v2 variable_def_
val map_cond_data_var : ( 'v -> 'v2 ) -> 'v condition_data_ -> 'v2 condition_data_
val cond_cats_to_set : int CatVarMap.t -> CatVarSet.t
val find_var_definition : program -> variable -> rule_data * variable_data
val get_var : string -> Variable.t Pos.VarNameToID.t -> Variable.t
val fresh_rule_num : unit -> int
val initial_undef_rule_id : rov_id
val find_var_by_name : program -> string Pos.marked -> variable

Get a variable for a given name or alias, because of SSA multiple variables share a name or alias. If an alias is provided, the variable returned is that with the lowest execution number. When a name is provided, then the variable with the highest execution number is returned.

val mast_to_catvar : 'a CatVarMap.t -> string Pos.marked list Pos.marked -> cat_variable
val expand_functions : program -> program

Calls expand_functions_expr on the whole program