CN: Rename Resultat to Or_TypeError

backend/cn/bin/main.ml

@@ -136,7 +136,7 @@ let with_well_formedness_check
      ail_prog:CF.GenTypes.genTypeCategory A.ail_program ->
      statement_locs:Cerb_location.t CStatements.LocMap.t ->
      paused:_ Typing.pause ->
-     unit Resultat.t)
+     unit Or_TypeError.t)
   =
   check_input_file filename;
   let prog, (markers_env, ail_prog), statement_locs =
@@ -157,7 +157,7 @@ let with_well_formedness_check
      | _ -> None);
   try
     let result =
-      let open Resultat in
+      let open Or_TypeError in
       let@ prog5 =
         Core_to_mucore.normalise_file
           ~inherit_loc:(not no_inherit_loc)
@@ -250,7 +250,7 @@ let well_formed
     ~no_inherit_loc
     ~magic_comment_char_dollar
     ~handle_error:(handle_type_error ~json ?output_dir ~serialize_json:json_trace)
-    ~f:(fun ~prog5:_ ~ail_prog:_ ~statement_locs:_ ~paused:_ -> Resultat.return ())
+    ~f:(fun ~prog5:_ ~ail_prog:_ ~statement_locs:_ ~paused:_ -> Or_TypeError.return ())
 
 
 let verify
@@ -429,7 +429,7 @@ let generate_executable_specs
                statement_locs
            with
            | e -> handle_error_with_user_guidance ~label:"CN-Exec" e);
-          Resultat.return ())
+          Or_TypeError.return ())
         ())
 
 
@@ -564,7 +564,7 @@ let run_tests
           if not dont_run then
             Unix.execv (Filename.concat output_dir "run_tests.sh") (Array.of_list []))
         ();
-      Resultat.return ())
+      Or_TypeError.return ())
 
 
 open Cmdliner

backend/cn/lib/builtins.ml

@@ -1,5 +1,5 @@
 module SBT = BaseTypes.Surface
-open Resultat
+open Or_TypeError
 open IndexTerms
 
 (* builtin function symbols *)

backend/cn/lib/check.ml

@@ -412,9 +412,9 @@ let check_conv_int loc ~expect ct arg =
 
 
 let check_against_core_bt loc msg2 cbt bt =
-  Typing.embed_resultat
+  Typing.fail_on_error
     (CoreTypeChecks.check_against_core_bt
-       (fun msg -> Resultat.fail { loc; msg = Generic (msg ^^ Pp.hardline ^^ msg2) })
+       (fun msg -> Or_TypeError.fail { loc; msg = Generic (msg ^^ Pp.hardline ^^ msg2) })
        cbt
        bt)
 
@@ -2678,7 +2678,7 @@ let time_check_c_functions (checked : c_function list) : (string * TypeErrors.t)
 let generate_lemmas lemmata o_lemma_mode =
   let@ global = get_global () in
   match o_lemma_mode with
-  | Some mode -> embed_resultat (Lemmata.generate global mode lemmata)
+  | Some mode -> fail_on_error (Lemmata.generate global mode lemmata)
   | None -> return ()
 
 (* TODO:

backend/cn/lib/compile.ml

@@ -34,8 +34,8 @@ type env =
     datatypes : BaseTypes.dt_info Sym.Map.t;
     datatype_constrs : BaseTypes.constr_info Sym.Map.t;
     tagDefs : (Cerb_frontend.Symbol.sym, Mu.tag_definition) Pmap.map;
-    fetch_enum_expr : Locations.t -> Sym.t -> unit CF.AilSyntax.expression Resultat.t;
-    fetch_typedef : Locations.t -> Sym.t -> CF.Ctype.ctype Resultat.t
+    fetch_enum_expr : Locations.t -> Sym.t -> unit CF.AilSyntax.expression Or_TypeError.t;
+    fetch_typedef : Locations.t -> Sym.t -> CF.Ctype.ctype Or_TypeError.t
   }
 
 let init_env tagDefs fetch_enum_expr fetch_typedef =
@@ -258,9 +258,9 @@ let register_cn_predicates env (defs : cn_predicate list) =
   List.fold_left aux env defs
 
 
-open Resultat
+open Or_TypeError
 
-open Effectful.Make (Resultat)
+open Effectful.Make (Or_TypeError)
 
 (* TODO: handle more kinds of constant expression *)
 let convert_enum_expr =
@@ -372,21 +372,21 @@ let add_datatype_infos env dts = ListM.fold_leftM add_datatype_info env dts
 module E = struct
   type evaluation_scope = string
 
-  type 'a m =
+  type 'a t =
     | Done of 'a
     | Error of TypeErrors.t
-    | ScopeExists of Locations.t * evaluation_scope * (bool -> 'a m)
+    | ScopeExists of Locations.t * evaluation_scope * (bool -> 'a t)
     | Value_of_c_variable of
-        Locations.t * Sym.t * evaluation_scope option * (IT.Surface.t option -> 'a m)
+        Locations.t * Sym.t * evaluation_scope option * (IT.Surface.t option -> 'a t)
     | Deref of
         Locations.t
         * IT.Surface.t
         * evaluation_scope option
-        * (IT.Surface.t option -> 'a m)
+        * (IT.Surface.t option -> 'a t)
 
   let return x = Done x
 
-  let rec bind (m : 'a m) (f : 'a -> 'b m) : 'b m =
+  let rec bind (m : 'a t) (f : 'a -> 'b t) : 'b t =
     match m with
     | Done x -> f x
     | Error err -> Error err
@@ -406,7 +406,7 @@ module E = struct
     Value_of_c_variable (loc, sym, scope, fun o_v_it -> Done o_v_it)
 
 
-  let liftResultat = function Result.Ok a -> Done a | Result.Error e -> Error e
+  let liftResult = function Result.Ok a -> Done a | Result.Error e -> Error e
 end
 
 let start_evaluation_scope = "start"
@@ -843,7 +843,7 @@ module EffectfulTranslation = struct
         return (IT (Cast (SBT.proj bt, expr), bt, loc))
       | CNExpr_call (fsym, exprs) ->
         let@ args = ListM.mapM self exprs in
-        let@ b = liftResultat (Builtins.apply_builtin_funs fsym args loc) in
+        let@ b = liftResult (Builtins.apply_builtin_funs fsym args loc) in
         (match b with
          | Some t -> return t
          | None ->
@@ -1015,7 +1015,7 @@ module EffectfulTranslation = struct
          | Some v -> return v)
       | CNExpr_value_of_c_atom (sym, C_kind_enum) ->
         assert (not (Sym.Set.mem sym locally_bound));
-        liftResultat (do_decode_enum env loc sym)
+        liftResult (do_decode_enum env loc sym)
     in
     trans None
 
@@ -1183,8 +1183,8 @@ module ET = EffectfulTranslation
 
 module Pure = struct
   let handle what = function
-    | E.Done x -> Resultat.return x
-    | E.Error e -> Resultat.fail e
+    | E.Done x -> Or_TypeError.return x
+    | E.Error e -> Or_TypeError.fail e
     | E.Value_of_c_variable (loc, _, _, _) ->
       let msg = !^what ^^^ !^"are not allowed to refer to (the state of) C variables." in
       fail { loc; msg = Generic msg }
@@ -1318,14 +1318,14 @@ module LocalState = struct
     List.fold_left (fun st (p, v) -> add_pointee_value p v st) st pvs
 
 
-  let handle { state; old_states } : 'a E.m -> 'a Resultat.m =
+  let handle { state; old_states } : 'a E.t -> 'a Or_TypeError.t =
     let state_for_scope = function
       | None -> state
       | Some s -> StringMap.find s old_states
     in
     let rec aux = function
-      | E.Done x -> Resultat.return x
-      | E.Error e -> Resultat.fail e
+      | E.Done x -> Or_TypeError.return x
+      | E.Error e -> Or_TypeError.fail e
       | E.Value_of_c_variable (loc, sym, scope, k) ->
         let variable_state = (state_for_scope scope).c_variable_state in
         let o_v =
@@ -1536,7 +1536,7 @@ module UsingLoads = struct
       fail { loc; msg }
 
 
-  let handle allocations old_states : Cnprog.t E.m -> Cnprog.t Resultat.m =
+  let handle allocations old_states : Cnprog.t E.t -> Cnprog.t Or_TypeError.t =
     let rec aux = function
       | E.Done x -> return x
       | E.Error e -> fail e

backend/cn/lib/coreTypeChecks.ml

@@ -1,6 +1,6 @@
 (* comparisons between CN base types and Core base types *)
 
-open Effectful.Make (Resultat)
+open Effectful.Make (Or_TypeError)
 
 module BT = BaseTypes
 open Cerb_frontend.Core

backend/cn/lib/core_to_mucore.ml

@@ -29,9 +29,9 @@ let get_loc_ = CF.Annot.get_loc_
 open CF.Core
 open Pp
 
-open Effectful.Make (Resultat)
+open Effectful.Make (Or_TypeError)
 
-let fail = Resultat.fail
+let fail = Or_TypeError.fail
 
 let do_ail_desugar_op desugar_state f =
   match f desugar_state with
@@ -646,7 +646,7 @@ let rec n_expr
   ((env, old_states), desugaring_things)
   (global_types, visible_objects_env)
   e
-  : unit Mucore.expr Resultat.m
+  : unit Mucore.expr Or_TypeError.t
   =
   let markers_env, cn_desugaring_state = desugaring_things in
   let (Expr (annots, pe)) = e in

backend/cn/lib/core_to_mucore.mli

@@ -5,7 +5,7 @@ val normalise_file
   :  inherit_loc:bool ->
   Cerb_frontend.Cabs_to_ail_effect.fin_markers_env * 'a Cerb_frontend.AilSyntax.sigma ->
   ('b, unit) Cerb_frontend.Milicore.mi_file ->
-  unit Mucore.file Resultat.m
+  unit Mucore.file Or_TypeError.t
 
 val arguments_of_at : ('a -> 'b) -> 'a ArgumentTypes.t -> 'b Mucore.arguments
 

backend/cn/lib/effectful.ml

@@ -1,9 +1,9 @@
 module type S = sig
-  type 'a m
+  type 'a t
 
-  val return : 'a -> 'a m
+  val return : 'a -> 'a t
 
-  val bind : 'a m -> ('a -> 'b m) -> 'b m
+  val bind : 'a t -> ('a -> 'b t) -> 'b t
 end
 
 module Make (T : S) = struct
@@ -12,9 +12,7 @@ module Make (T : S) = struct
   let ( let@ ) = T.bind
 
   module ListM = struct
-    open List
-
-    let rec mapM (f : 'a -> 'b m) (l : 'a list) : 'b list m =
+    let rec mapM (f : 'a -> 'b t) (l : 'a list) : 'b list t =
       match l with
       | [] -> return []
       | x :: xs ->
@@ -23,23 +21,23 @@ module Make (T : S) = struct
         return (y :: ys)
 
 
-    let mapfstM (f : 'a -> 'c m) (l : ('a * 'b) list) : ('c * 'b) list m =
+    let mapfstM (f : 'a -> 'c t) (l : ('a * 'b) list) : ('c * 'b) list t =
       mapM
         (fun (a, b) ->
           let@ c = f a in
           return (c, b))
         l
 
 
-    let mapsndM (f : 'b -> 'c m) (l : ('a * 'b) list) : ('a * 'c) list m =
+    let mapsndM (f : 'b -> 'c t) (l : ('a * 'b) list) : ('a * 'c) list t =
       mapM
         (fun (a, b) ->
           let@ c = f b in
           return (a, c))
         l
 
 
-    let mapiM (f : int -> 'a -> 'b m) (l : 'a list) : 'b list m =
+    let mapiM (f : int -> 'a -> 'b t) (l : 'a list) : 'b list t =
       let rec aux i l =
         match l with
         | [] -> return []
@@ -51,26 +49,26 @@ module Make (T : S) = struct
       aux 0 l
 
 
-    let map2M (f : 'a -> 'b -> 'c m) (l1 : 'a list) (l2 : 'b list) : 'c list m =
+    let map2M (f : 'a -> 'b -> 'c t) (l1 : 'a list) (l2 : 'b list) : 'c list t =
       let l12 = List.combine l1 l2 in
       mapM (Tools.uncurry f) l12
 
 
-    let iteriM (f : int -> 'a -> unit m) (l : 'a list) : unit m =
+    let iteriM (f : int -> 'a -> unit t) (l : 'a list) : unit t =
       let@ _ = mapiM f l in
       return ()
 
 
-    let iterM (f : 'a -> unit m) (l : 'a list) : unit m = iteriM (fun _ -> f) l
+    let iterM (f : 'a -> unit t) (l : 'a list) : unit t = iteriM (fun _ -> f) l
 
     let concat_mapM f l =
       let@ xs = mapM f l in
-      return (concat xs)
+      return (List.concat xs)
 
 
     let filter_mapM f l =
       let@ xs = mapM f l in
-      return (filter_map (fun x -> x) xs)
+      return (List.filter_map (fun x -> x) xs)
 
 
     let filterM f xs =
@@ -84,18 +82,17 @@ module Make (T : S) = struct
       return (List.map snd (List.filter fst ys))
 
 
-    let fold_leftM (f : 'a -> 'b -> 'c m) (a : 'a) (bs : 'b list) =
-      Stdlib.List.fold_left
+    let fold_leftM (f : 'a -> 'b -> 'c t) (a : 'a) (bs : 'b list) =
+      List.fold_left
         (fun aM b ->
           let@ a = aM in
           f a b)
         (return a)
         bs
 
 
-    (* maybe from Exception.lem *)
-    let fold_rightM (f : 'b -> 'a -> 'c m) (bs : 'b list) (a : 'a) =
-      Stdlib.List.fold_right
+    let fold_rightM (f : 'b -> 'a -> 'c t) (bs : 'b list) (a : 'a) =
+      List.fold_right
         (fun b aM ->
           let@ a = aM in
           f b a)
@@ -104,7 +101,7 @@ module Make (T : S) = struct
   end
 
   module PmapM = struct
-    let foldM (f : 'k -> 'x -> 'y -> 'y m) (map : ('k, 'x) Pmap.map) (init : 'y) : 'y m =
+    let foldM (f : 'k -> 'x -> 'y -> 'y t) (map : ('k, 'x) Pmap.map) (init : 'y) : 'y t =
       Pmap.fold
         (fun k v aM ->
           let@ a = aM in
@@ -113,8 +110,8 @@ module Make (T : S) = struct
         (return init)
 
 
-    let foldiM (f : int -> 'k -> 'x -> 'y -> 'y m) (map : ('k, 'x) Pmap.map) (init : 'y)
-      : 'y m
+    let foldiM (f : int -> 'k -> 'x -> 'y -> 'y t) (map : ('k, 'x) Pmap.map) (init : 'y)
+      : 'y t
       =
       ListM.fold_leftM
         (fun y (i, (k, x)) -> f i k x y)
@@ -131,8 +128,8 @@ module Make (T : S) = struct
         (return ())
 
 
-    let mapM (f : 'k -> 'v -> 'w m) (m : ('k, 'v) Pmap.map) (cmp : 'k -> 'k -> int)
-      : ('k, 'w) Pmap.map m
+    let mapM (f : 'k -> 'v -> 'w t) (m : ('k, 'v) Pmap.map) (cmp : 'k -> 'k -> int)
+      : ('k, 'w) Pmap.map t
       =
       foldM
         (fun k v m ->