1 files changed, 69 insertions, 170 deletions

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index dac64a9a..9a20a6cc 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -112,16 +112,16 @@ let reset_global_counters () =
   fun_call_id_counter := FunCallId.generator_zero;
   dummy_var_id_counter := DummyVarId.generator_zero
 
-(** Ancestor for {!var_binder} iter visitor *)
-class ['self] iter_var_binder_base =
+(** Ancestor for {!env} iter visitor *)
+class ['self] iter_env_base =
   object (_self : 'self)
     inherit [_] iter_abs
     method visit_var_id : 'env -> var_id -> unit = fun _ _ -> ()
     method visit_dummy_var_id : 'env -> dummy_var_id -> unit = fun _ _ -> ()
   end
 
-(** Ancestor for {!var_binder} map visitor *)
-class ['self] map_var_binder_base =
+(** Ancestor for {!env} map visitor *)
+class ['self] map_env_base =
   object (_self : 'self)
     inherit [_] map_abs
     method visit_var_id : 'env -> var_id -> var_id = fun _ x -> x
@@ -135,97 +135,29 @@ type var_binder = {
   index : var_id;  (** Unique variable identifier *)
   name : string option;  (** Possible name *)
 }
-[@@deriving
-  show,
-    visitors
-      {
-        name = "iter_var_binder";
-        variety = "iter";
-        ancestors = [ "iter_var_binder_base" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      },
-    visitors
-      {
-        name = "map_var_binder";
-        variety = "map";
-        ancestors = [ "map_var_binder_base" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      }]
 
 (** A binder, for a "real" variable or a dummy variable *)
-type binder = VarBinder of var_binder | DummyBinder of dummy_var_id
-[@@deriving
-  show,
-    visitors
-      {
-        name = "iter_binder";
-        variety = "iter";
-        ancestors = [ "iter_var_binder" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      },
-    visitors
-      {
-        name = "map_binder";
-        variety = "map";
-        ancestors = [ "map_var_binder" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      }]
-
-(** Ancestor for {!env_elem} iter visitor *)
-class ['self] iter_env_elem_base =
-  object (_self : 'self)
-    inherit [_] iter_binder
-  end
-
-(** Ancestor for {!env_elem} map visitor *)
-class ['self] map_env_elem_base =
-  object (_self : 'self)
-    inherit [_] map_binder
-  end
+and binder = BVar of var_binder | BDummy of dummy_var_id
 
 (** Environment value: mapping from variable to value, abstraction (only
     used in symbolic mode) or stack frame delimiter.
-    
-    TODO: rename Var (-> Binding?)
  *)
-type env_elem =
-  | Var of binder * typed_value
+and env_elem =
+  | EBinding of binder * typed_value
       (** Variable binding - the binder is None if the variable is a dummy variable
           (we use dummy variables to store temporaries while doing bookkeeping such
            as ending borrows for instance). *)
-  | Abs of abs
-  | Frame
-[@@deriving
-  show,
-    visitors
-      {
-        name = "iter_env_elem";
-        variety = "iter";
-        ancestors = [ "iter_env_elem_base" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      },
-    visitors
-      {
-        name = "map_env_elem";
-        variety = "map";
-        ancestors = [ "map_env_elem_base" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      }]
+  | EAbs of abs
+  | EFrame
 
-type env = env_elem list
+and env = env_elem list
 [@@deriving
   show,
     visitors
       {
         name = "iter_env";
         variety = "iter";
-        ancestors = [ "iter_env_elem" ];
+        ancestors = [ "iter_env_base" ];
         nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       },
@@ -233,7 +165,7 @@ type env = env_elem list
       {
         name = "map_env";
         variety = "map";
-        ancestors = [ "map_env_elem" ];
+        ancestors = [ "map_env_base" ];
         nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       }]
@@ -280,48 +212,20 @@ type decls_ctx = {
 [@@deriving show]
 
 (** A reference to a trait associated type *)
-type 'r trait_type_ref = { trait_ref : 'r trait_ref; type_name : string }
-[@@deriving show, ord]
-
-type etrait_type_ref = erased_region trait_type_ref [@@deriving show, ord]
-
-type rtrait_type_ref = Types.RegionId.id Types.region trait_type_ref
-[@@deriving show, ord]
-
-type strait_type_ref = Types.RegionVarId.id Types.region trait_type_ref
+type trait_type_ref = { trait_ref : trait_ref; type_name : string }
 [@@deriving show, ord]
 
 (* TODO: correctly use the functors so as not to have a duplication below *)
-module ETraitTypeRefOrd = struct
-  type t = etrait_type_ref
+module TraitTypeRefOrd = struct
+  type t = trait_type_ref
 
-  let compare = compare_etrait_type_ref
-  let to_string = show_etrait_type_ref
-  let pp_t = pp_etrait_type_ref
-  let show_t = show_etrait_type_ref
+  let compare = compare_trait_type_ref
+  let to_string = show_trait_type_ref
+  let pp_t = pp_trait_type_ref
+  let show_t = show_trait_type_ref
 end
 
-module RTraitTypeRefOrd = struct
-  type t = rtrait_type_ref
-
-  let compare = compare_rtrait_type_ref
-  let to_string = show_rtrait_type_ref
-  let pp_t = pp_rtrait_type_ref
-  let show_t = show_rtrait_type_ref
-end
-
-module STraitTypeRefOrd = struct
-  type t = strait_type_ref
-
-  let compare = compare_strait_type_ref
-  let to_string = show_strait_type_ref
-  let pp_t = pp_strait_type_ref
-  let show_t = show_strait_type_ref
-end
-
-module ETraitTypeRefMap = Collections.MakeMap (ETraitTypeRefOrd)
-module RTraitTypeRefMap = Collections.MakeMap (RTraitTypeRefOrd)
-module STraitTypeRefMap = Collections.MakeMap (STraitTypeRefOrd)
+module TraitTypeRefMap = Collections.MakeMap (TraitTypeRefOrd)
 
 (** Evaluation context *)
 type eval_ctx = {
@@ -337,25 +241,10 @@ type eval_ctx = {
       (** The map from const generic vars to their values. Those values
           can be symbolic values or concrete values (in the latter case:
           if we run in interpreter mode) *)
-  norm_trait_etypes : ety ETraitTypeRefMap.t;
+  norm_trait_types : ty TraitTypeRefMap.t;
       (** The normalized trait types (a map from trait types to their representatives).
-          Note that this doesn't support account higher-order types. *)
-  norm_trait_rtypes : rty RTraitTypeRefMap.t;
-      (** We need this because we manipulate two kinds of types.
-          Note that we actually forbid regions from appearing both in the trait
-          references and in the constraints given to the associated types,
-          meaning that we don't have to worry about mismatches due to changes
-          in region ids.
-
-          TODO: how not to duplicate?
-       *)
-  norm_trait_stypes : sty STraitTypeRefMap.t;
-      (** We sometimes need to normalize types in non-instantiated signatures.
-
-          Note that we either need to use the etypes/rtypes maps, or the stypes map.
-          This means that we either compute the maps for etypes and rtypes, or compute
-          the one for stypes (we don't always compute and carry all the maps).
-       *)
+          Note that this doesn't take into account higher-order type constraints
+          (of the shape `for<'a> ...`). *)
   env : env;
   ended_regions : RegionId.Set.t;
 }
@@ -389,10 +278,10 @@ let env_lookup_var (env : env) (vid : VarId.id) : var_binder * typed_value =
     match env with
     | [] ->
         raise (Invalid_argument ("Variable not found: " ^ VarId.to_string vid))
-    | Var (VarBinder var, v) :: env' ->
+    | EBinding (BVar var, v) :: env' ->
         if var.index = vid then (var, v) else lookup env'
-    | (Var (DummyBinder _, _) | Abs _) :: env' -> lookup env'
-    | Frame :: _ -> raise (Failure "End of frame")
+    | (EBinding (BDummy _, _) | EAbs _) :: env' -> lookup env'
+    | EFrame :: _ -> raise (Failure "End of frame")
   in
   lookup env
 
@@ -440,11 +329,11 @@ let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env =
   let rec update env =
     match env with
     | [] -> raise (Failure "Unexpected")
-    | Var ((VarBinder b as var), v) :: env' ->
-        if b.index = vid then Var (var, nv) :: env'
-        else Var (var, v) :: update env'
-    | ((Var (DummyBinder _, _) | Abs _) as ee) :: env' -> ee :: update env'
-    | Frame :: _ -> raise (Failure "End of frame")
+    | EBinding ((BVar b as var), v) :: env' ->
+        if b.index = vid then EBinding (var, nv) :: env'
+        else EBinding (var, v) :: update env'
+    | ((EBinding (BDummy _, _) | EAbs _) as ee) :: env' -> ee :: update env'
+    | EFrame :: _ -> raise (Failure "End of frame")
   in
   update env
 
@@ -466,9 +355,9 @@ let ctx_update_var_value (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) :
     is important).
 *)
 let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
-  assert (var.var_ty = v.ty);
+  assert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty);
   let bv = var_to_binder var in
-  { ctx with env = Var (VarBinder bv, v) :: ctx.env }
+  { ctx with env = EBinding (BVar bv, v) :: ctx.env }
 
 (** Push a list of variables.
 
@@ -488,11 +377,12 @@ let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
              vars)));
   assert (
     List.for_all
-      (fun (var, (value : typed_value)) -> var.var_ty = value.ty)
+      (fun (var, (value : typed_value)) ->
+        TypesUtils.ty_is_ety var.var_ty && var.var_ty = value.ty)
       vars);
   let vars =
     List.map
-      (fun (var, value) -> Var (VarBinder (var_to_binder var), value))
+      (fun (var, value) -> EBinding (BVar (var_to_binder var), value))
       vars
   in
   let vars = List.rev vars in
@@ -501,7 +391,7 @@ let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
 (** Push a dummy variable in the context's environment. *)
 let ctx_push_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) (v : typed_value)
     : eval_ctx =
-  { ctx with env = Var (DummyBinder vid, v) :: ctx.env }
+  { ctx with env = EBinding (BDummy vid, v) :: ctx.env }
 
 (** Remove a dummy variable from a context's environment. *)
 let ctx_remove_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) :
@@ -509,7 +399,7 @@ let ctx_remove_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) :
   let rec remove_var (env : env) : env * typed_value =
     match env with
     | [] -> raise (Failure "Could not lookup a dummy variable")
-    | Var (DummyBinder vid', v) :: env when vid' = vid -> (env, v)
+    | EBinding (BDummy vid', v) :: env when vid' = vid -> (env, v)
     | ee :: env ->
         let env, v = remove_var env in
         (ee :: env, v)
@@ -522,27 +412,36 @@ let ctx_lookup_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) : typed_value =
   let rec lookup_var (env : env) : typed_value =
     match env with
     | [] -> raise (Failure "Could not lookup a dummy variable")
-    | Var (DummyBinder vid', v) :: _env when vid' = vid -> v
+    | EBinding (BDummy vid', v) :: _env when vid' = vid -> v
     | _ :: env -> lookup_var env
   in
   lookup_var ctx.env
 
+let erase_regions (ty : ty) : ty =
+  let v =
+    object
+      inherit [_] map_ty
+      method! visit_region _ _ = RErased
+    end
+  in
+  v#visit_ty () ty
+
 (** Push an uninitialized variable (which thus maps to {!constructor:Values.value.Bottom}) *)
 let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx =
-  ctx_push_var ctx var (mk_bottom var.var_ty)
+  ctx_push_var ctx var (mk_bottom (erase_regions var.var_ty))
 
 (** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.Bottom}) *)
 let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx =
-  let vars = List.map (fun v -> (v, mk_bottom v.var_ty)) vars in
+  let vars = List.map (fun v -> (v, mk_bottom (erase_regions v.var_ty))) vars in
   ctx_push_vars ctx vars
 
 let env_find_abs (env : env) (pred : V.abs -> bool) : V.abs option =
   let rec lookup env =
     match env with
     | [] -> None
-    | Var (_, _) :: env' -> lookup env'
-    | Abs abs :: env' -> if pred abs then Some abs else lookup env'
-    | Frame :: env' -> lookup env'
+    | EBinding (_, _) :: env' -> lookup env'
+    | EAbs abs :: env' -> if pred abs then Some abs else lookup env'
+    | EFrame :: env' -> lookup env'
   in
   lookup env
 
@@ -558,17 +457,17 @@ let env_remove_abs (env : env) (abs_id : V.AbstractionId.id) :
   let rec remove (env : env) : env * V.abs option =
     match env with
     | [] -> raise (Failure "Unreachable")
-    | Frame :: _ -> (env, None)
-    | Var (bv, v) :: env ->
+    | EFrame :: _ -> (env, None)
+    | EBinding (bv, v) :: env ->
         let env, abs_opt = remove env in
-        (Var (bv, v) :: env, abs_opt)
-    | Abs abs :: env ->
+        (EBinding (bv, v) :: env, abs_opt)
+    | EAbs abs :: env ->
         if abs.abs_id = abs_id then (env, Some abs)
         else
           let env, abs_opt = remove env in
           (* Update the parents set *)
           let parents = V.AbstractionId.Set.remove abs_id abs.parents in
-          (Abs { abs with V.parents } :: env, abs_opt)
+          (EAbs { abs with V.parents } :: env, abs_opt)
   in
   remove env
 
@@ -584,12 +483,12 @@ let env_subst_abs (env : env) (abs_id : V.AbstractionId.id) (nabs : V.abs) :
   let rec update (env : env) : env * V.abs option =
     match env with
     | [] -> raise (Failure "Unreachable")
-    | Frame :: _ -> (* We're done *) (env, None)
-    | Var (bv, v) :: env ->
+    | EFrame :: _ -> (* We're done *) (env, None)
+    | EBinding (bv, v) :: env ->
         let env, opt_abs = update env in
-        (Var (bv, v) :: env, opt_abs)
-    | Abs abs :: env ->
-        if abs.abs_id = abs_id then (Abs nabs :: env, Some abs)
+        (EBinding (bv, v) :: env, opt_abs)
+    | EAbs abs :: env ->
+        if abs.abs_id = abs_id then (EAbs nabs :: env, Some abs)
         else
           let env, opt_abs = update env in
           (* Update the parents set *)
@@ -600,7 +499,7 @@ let env_subst_abs (env : env) (abs_id : V.AbstractionId.id) (nabs : V.abs) :
               V.AbstractionId.Set.add nabs.abs_id parents
             else parents
           in
-          (Abs { abs with V.parents } :: env, opt_abs)
+          (EAbs { abs with V.parents } :: env, opt_abs)
   in
   update env
 
@@ -641,7 +540,7 @@ class ['self] iter_frame =
       fun acc env ->
         match env with
         | [] -> ()
-        | Frame :: _ -> (* We stop here *) ()
+        | EFrame :: _ -> (* We stop here *) ()
         | em :: env ->
             self#visit_env_elem acc em;
             self#visit_env acc env
@@ -656,7 +555,7 @@ class ['self] map_frame_concrete =
       fun acc env ->
         match env with
         | [] -> []
-        | Frame :: env -> (* We stop here *) Frame :: env
+        | EFrame :: env -> (* We stop here *) EFrame :: env
         | em :: env ->
             let em = self#visit_env_elem acc em in
             let env = self#visit_env acc env in
@@ -686,17 +585,17 @@ class ['self] map_eval_ctx =
 let env_iter_abs (f : V.abs -> unit) (env : env) : unit =
   List.iter
     (fun (ee : env_elem) ->
-      match ee with Var _ | Frame -> () | Abs abs -> f abs)
+      match ee with EBinding _ | EFrame -> () | EAbs abs -> f abs)
     env
 
 let env_map_abs (f : V.abs -> V.abs) (env : env) : env =
   List.map
     (fun (ee : env_elem) ->
-      match ee with Var _ | Frame -> ee | Abs abs -> Abs (f abs))
+      match ee with EBinding _ | EFrame -> ee | EAbs abs -> EAbs (f abs))
     env
 
 let env_filter_abs (f : V.abs -> bool) (env : env) : env =
   List.filter
     (fun (ee : env_elem) ->
-      match ee with Var _ | Frame -> true | Abs abs -> f abs)
+      match ee with EBinding _ | EFrame -> true | EAbs abs -> f abs)
     env