Documentation

Author: Stevendeo

src/mlang/index.mld

@@ -28,10 +28,25 @@ and basically all programs typecheck ; however {!module: Mlang.M_frontend.Valida
   Mlang.M_ir.Com
   Mlang.M_ir.Format_mir
   Mlang.M_ir.Mir
-  Mlang.M_ir.Mir_interpreter
   Mlang.M_ir.Mir_number
   Mlang.M_ir.Mir_roundops }
 
+{1 Interpreter}
+
+The intepreter is the reference for the M semantics. The C code Mlang generates must
+follow it.
+The main interpreter module is {!module: Mlang.Mir_interpreter.Eval} which defines two
+functions: {!Mlang.Mir_interpreter.Eval.evaluate_program} and {!Mlang.Mir_interpreter.Eval.evaluate_expr}. It also defines several modules that evaluates programs and expression
+with different float precisions.
+
+{!modules:
+  Mlang.Mir_interpreter.Anomalies
+  Mlang.Mir_interpreter.Context
+  Mlang.Mir_interpreter.Eval
+  Mlang.Mir_interpreter.Functions
+  Mlang.Mir_interpreter.Print
+  Mlang.Mir_interpreter.Types }
+
 {1 Testing}
 
 Mlang comes with a testing framework for M programs that is based on

src/mlang/m_ir/mir.mli

@@ -22,14 +22,13 @@
     - Constants have been inlined.
     - Loops (FunCallLoop, Loop) have been unrolled.
     - Chaining, domain and verification calculations have been unified into
-    Target calculations.
-    This filtering is performed by {!M_frontend.Expander}, {!M_frontend.Validator} and
-    {!M_frontend.Mast_to_mir}.
+      Target calculations. This filtering is performed by
+      {!M_frontend.Expander}, {!M_frontend.Validator} and
+      {!M_frontend.Mast_to_mir}.
 
-    The structural difference between {!M_frontend.Mast} and Mir common types are
-    the replacement of {!Mir.Com.m_var_name} by {!M_ir.Com.Var.t} and
-    {!M_frontend.Mast.error_name} by {!M_ir.Com.Error.t}.
- *)
+    The structural difference between {!M_frontend.Mast} and Mir common types
+    are the replacement of {!Mir.Com.m_var_name} by {!M_ir.Com.Var.t} and
+    {!M_frontend.Mast.error_name} by {!M_ir.Com.Error.t}. *)
 
 type set_value = Com.Var.t Com.set_value
 
@@ -64,8 +63,7 @@ type stats = {
   max_nb_args : int;
   table_map : Com.Var.t IntMap.t;
 }
-(** A set of constants relative to the program and its selected
-    applications. *)
+(** A set of constants relative to the program and its selected applications. *)
 
 type program = {
   program_safe_prefix : string;

src/mlang/m_ir/mir_number.ml

@@ -234,8 +234,11 @@ MakeComparable (struct
   let is_nan_or_inf x = not (Mpfrf.number_p x)
 end)
 
-module IntervalNumber : NumberInterface = MakeComparable (struct
-  type t = { down : Mpfrf.t; up : Mpfrf.t }
+type interval = { down : Mpfrf.t; up : Mpfrf.t }
+
+module IntervalNumber : NumberInterface with type t = interval =
+MakeComparable (struct
+  type t = interval
 
   let v (x : Mpfrf.t) (y : Mpfrf.t) : t = { down = x; up = y }
 

src/mlang/m_ir/mir_number.mli

@@ -14,6 +14,8 @@
    You should have received a copy of the GNU General Public License along with
    this program. If not, see <https://www.gnu.org/licenses/>. *)
 
+type interval = { down : Mpfrf.t; up : Mpfrf.t }
+
 module type NumberInterface = sig
   type t
 
@@ -68,8 +70,8 @@ module type NumberInterface = sig
   val is_zero : t -> bool
 
   val compare : ?epsilon:float -> Com.comp_op -> t -> t -> bool
-  (** Returns the comparison between two numbers in the precision context
-    of the current configuration. *)
+  (** Returns the comparison between two numbers in the precision context of the
+      current configuration. *)
 end
 
 module RegularFloatNumber : NumberInterface with type t = float
@@ -78,7 +80,7 @@ val mpfr_floor : Mpfrf.t -> Mpfrf.t
 
 module MPFRNumber : NumberInterface with type t = Mpfrf.t
 
-module IntervalNumber : NumberInterface
+module IntervalNumber : NumberInterface with type t = interval
 
 module RationalNumber : NumberInterface with type t = Mpqf.t
 

src/mlang/mir_interpreter/anomalies.mli

@@ -1,18 +1,17 @@
 val raise : 'a Types.ctx -> M_ir.Com.Error.t -> string option -> bool
-(** Adds the anomaly to the context and returns [true] if the said anomaly
-    is blocking, [false] otherwise. *)
+(** Adds the anomaly to the context and returns [true] if the said anomaly is
+    blocking, [false] otherwise. *)
 
 val clean : 'a Types.ctx -> unit
-(** Cleans the context from its unfinalized and unarchived
-    anomalies. *)
+(** Cleans the context from its unfinalized and unarchived anomalies. *)
 
 val clean_finalized : 'a Types.ctx -> unit
 (** Cleans the context from its finalized anomalies. *)
 
 val finalize : mode_corr:bool -> 'a Types.ctx -> unit
-(** Moves the raised anomalies to the finalized anomalies (and the
-    archived anomalies if [mode_corr] is [true]). *)
+(** Moves the raised anomalies to the finalized anomalies (and the archived
+    anomalies if [mode_corr] is [true]). *)
 
 val export : mode_corr:bool -> 'a Types.ctx -> unit
-(** Moves the finalized anomalies to the exported anomalies (and the
-    archived anomalies if [mode_corr] is [true]). *)
+(** Moves the finalized anomalies to the exported anomalies (and the archived
+    anomalies if [mode_corr] is [true]). *)

src/mlang/mir_interpreter/context.mli

@@ -11,14 +11,12 @@ module type S = sig
     M_ir.Com.Var.t ->
     M_ir.Com.variable_space * M_ir.Com.Var.t * int
   (** Returns the variable identifier and its space, with an offset integer.
-      This offset integer is 0 for TGV variables
-   *)
+      This offset integer is 0 for TGV variables *)
 
   val get_var_tab :
     custom_float Types.ctx -> M_ir.Com.Var.t -> int -> M_ir.Com.Var.t
-  (** [get_var_tab ctx vs v i]
-      Each cell of a table is a separate variable. This function
-      returns the variable representing the cell [i] in table [v].
+  (** [get_var_tab ctx vs v i] Each cell of a table is a separate variable. This
+      function returns the variable representing the cell [i] in table [v].
       Fails if the variable in argument is not a table. *)
 
   val get_var_value_org :
@@ -110,9 +108,8 @@ val empty_ctx :
 (** [empty_ctx ?inputs ?events p]
 
     Creates a fresh context for executing the program [p] or expressions within
-    the context of [p] (for example, with variables declared in [p].
-    Parameters [inputs] and [events] are required for interpreting the whole
-    program. *)
+    the context of [p] (for example, with variables declared in [p]. Parameters
+    [inputs] and [events] are required for interpreting the whole program. *)
 
 module Make (N : M_ir.Mir_number.NumberInterface) :
   S with type custom_float := N.t

src/mlang/mir_interpreter/eval.ml

@@ -35,8 +35,8 @@ module type S = sig
   (** Evaluates an expression. *)
 
   val evaluate_program : ctx -> unit
-  (** Evaluates a whole program. Proper initialisation of inputs and events
-      is required before calling this function (through [update_ctx_with_inputs]
+  (** Evaluates a whole program. Proper initialisation of inputs and events is
+      required before calling this function (through [update_ctx_with_inputs]
       and [update_ctx_with_events]. *)
 
   (** {2 Helpers} *)

src/mlang/mir_interpreter/eval.mli

@@ -2,6 +2,30 @@
 
 val exit_on_rte : bool ref
 
+(** {2 Generic evaluation functions} *)
+
+val evaluate_program :
+  p:M_ir.Mir.program ->
+  inputs:M_ir.Com.literal M_ir.Com.Var.Map.t ->
+  events:(M_ir.Com.literal, M_ir.Com.Var.t) M_ir.Com.event_value StrMap.t list ->
+  sort:Config.value_sort ->
+  round_ops:Config.round_ops ->
+  M_ir.Com.literal M_ir.Com.Var.Map.t * M_ir.Com.Error.Set.t
+(** Evaluates a whole program and returns the given back variables, as well as
+    the set of anomalies. The evaluation engine is selected from [sort] and
+    [roundops]. *)
+
+val evaluate_expr :
+  p:M_ir.Mir.program ->
+  e:M_ir.Mir.expression Pos.marked ->
+  sort:Config.value_sort ->
+  round_ops:Config.round_ops ->
+  M_ir.Com.literal
+(** Evaluates a single expression. The evaluation engine is selected from [sort]
+    and [roundops]. *)
+
+(** {2 Generic module type} *)
+
 module type S = sig
   type custom_float
 
@@ -16,8 +40,8 @@ module type S = sig
   (** Evaluates an expression. *)
 
   val evaluate_program : ctx -> unit
-  (** Evaluates a whole program. Proper initialisation of inputs and events
-      is required before calling this function (through [update_ctx_with_inputs]
+  (** Evaluates a whole program. Proper initialisation of inputs and events is
+      required before calling this function (through [update_ctx_with_inputs]
       and [update_ctx_with_events]. *)
 
   (** {2 Helpers} *)
@@ -47,52 +71,47 @@ module Make
 (** These modules are instanes of Make with modules defined in
     {!module: M_ir.Mir_number} and {!module: M_ir.Mir_roundops}. *)
 
+(** Float with default rounding strategy. *)
 module FloatDefInterp : S with type custom_float = float
 
+(** Float with multithread rounding strategy. *)
 module FloatMultInterp : S with type custom_float = float
 
+(** Float with mainframe rounding strategy. *)
 module FloatMfInterp : S with type custom_float = float
 
+(** Multiple-precision floating-point with default rounding strategy. *)
 module MPFRDefInterp : S with type custom_float = Mpfrf.t
 
+(** Multiple-precision floating-point with multithread rounding strategy. *)
 module MPFRMultInterp : S with type custom_float = Mpfrf.t
 
+(** Multiple-precision floating-point with mainframe rounding strategy. *)
 module MPFRMfInterp : S with type custom_float = Mpfrf.t
 
+(** Multiple precision integer arithmetic with default rounding strategy. *)
 module BigIntDefInterp : S with type custom_float = Mpzf.t
 
+(** Multiple precision integer arithmetic with multihtread rounding strategy. *)
 module BigIntMultInterp : S with type custom_float = Mpzf.t
 
+(** Multiple precision integer arithmetic with mainframe rounding strategy. *)
 module BigIntMfInterp : S with type custom_float = Mpzf.t
 
-module IntvDefInterp : S
+(** Multiple-precision floating-point intervals with default rounding strategy. *)
+module IntvDefInterp : S with type custom_float = M_ir.Mir_number.interval
 
-module IntvMultInterp : S
+(** Multiple-precision floating-point intervals with multithread rounding strategy. *)
+module IntvMultInterp : S with type custom_float = M_ir.Mir_number.interval
 
-module IntvMfInterp : S
+(** Multiple-precision floating-point intervals with mainframe rounding strategy. *)
+module IntvMfInterp : S with type custom_float = M_ir.Mir_number.interval
 
+(** Multiple-precision rationals with default rounding strategy. *)
 module RatDefInterp : S with type custom_float = Mpqf.t
 
+(** Multiple-precision rationals with multithread rounding strategy. *)
 module RatMultInterp : S with type custom_float = Mpqf.t
 
+(** Multiple-precision rationals with mainframe rounding strategy. *)
 module RatMfInterp : S with type custom_float = Mpqf.t
-
-val evaluate_program :
-  p:M_ir.Mir.program ->
-  inputs:M_ir.Com.literal M_ir.Com.Var.Map.t ->
-  events:(M_ir.Com.literal, M_ir.Com.Var.t) M_ir.Com.event_value StrMap.t list ->
-  sort:Config.value_sort ->
-  round_ops:Config.round_ops ->
-  M_ir.Com.literal M_ir.Com.Var.Map.t * M_ir.Com.Error.Set.t
-(** Evaluates a whole program and returns the given back variables, as
-    well as the set of anomalies.
-    The evaluation engine is selected from [sort] and [roundops]. *)
-
-val evaluate_expr :
-  p:M_ir.Mir.program ->
-  e:M_ir.Mir.expression Pos.marked ->
-  sort:Config.value_sort ->
-  round_ops:Config.round_ops ->
-  M_ir.Com.literal
-(** Evaluates a single expression.
-    The evaluation engine is selected from [sort] and [roundops]. *)