diff options
| -rw-r--r-- | src/Values.ml | 243 |
1 files changed, 242 insertions, 1 deletions
diff --git a/src/Values.ml b/src/Values.ml index 7c7f6d1a..68d9aa7e 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -65,13 +65,25 @@ type symbolic_proj_comp = { regions *but* the ones which are listed in the projector. *) -(** Polymorphic visitor *) +(** Polymorphic iter visitor *) class virtual ['self] iter_'r_ty_base = object (self : 'self) method visit_ty : 'env 'r. ('env -> 'r -> unit) -> 'env -> 'r ty -> unit = fun _visit_'r _env _ty -> () end +(** Polymorphic map visitor *) +class virtual ['self] map_'r_ty_base = + object (self : 'self) + method visit_ty + : 'env 'r_0 'r_1. ('env -> 'r_0 -> 'r_1) -> 'env -> 'r_0 ty -> 'r_1 ty = + fun _visit_'r _env ty -> + (* We should use a ty visitor, but in practice we don't need to + * visit types, and for the non-generic visit methods (which will + * preserve 'r_0) we will override this method with identity *) + raise Errors.Unimplemented + end + (** A generic, untyped value, used in the environments. Parameterized by: @@ -112,8 +124,169 @@ and ('r, 'sv, 'bc, 'lc) g_typed_value = { polymorphic = true; (* Heirs expect a polymorphic class *) concrete = true; + }, + visitors + { + name = "map_g_typed_value"; + variety = "map"; + ancestors = [ "map_'r_ty_base" ]; + polymorphic = true; + (* Heirs expect a polymorphic class *) + concrete = true; }] +(*class ['self] map_g_typed_value = + object (self : 'self) + inherit [_] VisitorsRuntime.map + + inherit [_] map_'r_ty_base + + method visit_Concrete + : 'env 'r_0 'r_1 'sv_0 'sv_1 'bc_0 'bc_1 'lc_0 'lc_1. + ('env -> 'r_0 -> 'r_1) -> + ('env -> 'sv_0 -> 'sv_1) -> + ('env -> 'bc_0 -> 'bc_1) -> + ('env -> 'lc_0 -> 'lc_1) -> + 'env -> + _ -> + ('r_1, 'sv_1, 'bc_1, 'lc_1) g_value = + fun visit_'r visit_'sv visit_'bc visit_'lc env _visitors_c0 -> + let _visitors_r0 = + (fun _visitors_this -> _visitors_this) _visitors_c0 + in + Concrete _visitors_r0 + + method visit_Adt + : 'env 'r_0 'r_1 'sv_0 'sv_1 'bc_0 'bc_1 'lc_0 'lc_1. + ('env -> 'r_0 -> 'r_1) -> + ('env -> 'sv_0 -> 'sv_1) -> + ('env -> 'bc_0 -> 'bc_1) -> + ('env -> 'lc_0 -> 'lc_1) -> + 'env -> + ('r_0, 'sv_0, 'bc_0, 'lc_0) g_adt_value -> + ('r_1, 'sv_1, 'bc_1, 'lc_1) g_value = + fun visit_'r visit_'sv visit_'bc visit_'lc env _visitors_c0 -> + let _visitors_r0 = + self#visit_g_adt_value visit_'r visit_'sv visit_'bc visit_'lc env + _visitors_c0 + in + Adt _visitors_r0 + + method visit_Bottom + : 'env 'r_0 'r_1 'sv_0 'sv_1 'bc_0 'bc_1 'lc_0 'lc_1. + ('env -> 'r_0 -> 'r_1) -> + ('env -> 'sv_0 -> 'sv_1) -> + ('env -> 'bc_0 -> 'bc_1) -> + ('env -> 'lc_0 -> 'lc_1) -> + 'env -> + ('r_1, 'sv_1, 'bc_1, 'lc_1) g_value = + fun visit_'r visit_'sv visit_'bc visit_'lc env -> Bottom + + method visit_Borrow + : 'env 'r_0 'r_1 'sv_0 'sv_1 'bc_0 'bc_1 'lc_0 'lc_1. + ('env -> 'r_0 -> 'r_1) -> + ('env -> 'sv_0 -> 'sv_1) -> + ('env -> 'bc_0 -> 'bc_1) -> + ('env -> 'lc_0 -> 'lc_1) -> + 'env -> + 'bc_0 -> + ('r_1, 'sv_1, 'bc_1, 'lc_1) g_value = + fun visit_'r visit_'sv visit_'bc visit_'lc env _visitors_c0 -> + let _visitors_r0 = visit_'bc env _visitors_c0 in + Borrow _visitors_r0 + + method visit_Loan + : 'env 'r_0 'r_1 'sv_0 'sv_1 'bc_0 'bc_1 'lc_0 'lc_1. + ('env -> 'r_0 -> 'r_1) -> + ('env -> 'sv_0 -> 'sv_1) -> + ('env -> 'bc_0 -> 'bc_1) -> + ('env -> 'lc_0 -> 'lc_1) -> + 'env -> + 'lc_0 -> + ('r_1, 'sv_1, 'bc_1, 'lc_1) g_value = + fun visit_'r visit_'sv visit_'bc visit_'lc env _visitors_c0 -> + let _visitors_r0 = visit_'lc env _visitors_c0 in + Loan _visitors_r0 + + method visit_Symbolic + : 'env 'r_0 'r_1 'sv_0 'sv_1 'bc_0 'bc_1 'lc_0 'lc_1. + ('env -> 'r_0 -> 'r_1) -> + ('env -> 'sv_0 -> 'sv_1) -> + ('env -> 'bc_0 -> 'bc_1) -> + ('env -> 'lc_0 -> 'lc_1) -> + 'env -> + 'sv_0 -> + ('r_1, 'sv_1, 'bc_1, 'lc_1) g_value = + fun visit_'r visit_'sv visit_'bc visit_'lc env _visitors_c0 -> + let _visitors_r0 = visit_'sv env _visitors_c0 in + Symbolic _visitors_r0 + + method visit_g_value + : 'env 'r_0 'r_1 'sv_0 'sv_1 'bc_0 'bc_1 'lc_0 'lc_1. + ('env -> 'r_0 -> 'r_1) -> + ('env -> 'sv_0 -> 'sv_1) -> + ('env -> 'bc_0 -> 'bc_1) -> + ('env -> 'lc_0 -> 'lc_1) -> + 'env -> + ('r_0, 'sv_0, 'bc_0, 'lc_0) g_value -> + ('r_1, 'sv_1, 'bc_1, 'lc_1) g_value = + fun visit_'r visit_'sv visit_'bc visit_'lc env _visitors_this -> + match _visitors_this with + | Concrete _visitors_c0 -> + self#visit_Concrete visit_'r visit_'sv visit_'bc visit_'lc env + _visitors_c0 + | Adt _visitors_c0 -> + self#visit_Adt visit_'r visit_'sv visit_'bc visit_'lc env + _visitors_c0 + | Bottom -> self#visit_Bottom visit_'r visit_'sv visit_'bc visit_'lc env + | Borrow _visitors_c0 -> + self#visit_Borrow visit_'r visit_'sv visit_'bc visit_'lc env + _visitors_c0 + | Loan _visitors_c0 -> + self#visit_Loan visit_'r visit_'sv visit_'bc visit_'lc env + _visitors_c0 + | Symbolic _visitors_c0 -> + self#visit_Symbolic visit_'r visit_'sv visit_'bc visit_'lc env + _visitors_c0 + + method visit_g_adt_value + : 'env 'r_0 'r_1 'sv_0 'sv_1 'bc_0 'bc_1 'lc_0 'lc_1. + ('env -> 'r_0 -> 'r_1) -> + ('env -> 'sv_0 -> 'sv_1) -> + ('env -> 'bc_0 -> 'bc_1) -> + ('env -> 'lc_0 -> 'lc_1) -> + 'env -> + ('r_0, 'sv_0, 'bc_0, 'lc_0) g_adt_value -> + ('r_1, 'sv_1, 'bc_1, 'lc_1) g_adt_value = + fun visit_'r visit_'sv visit_'bc visit_'lc env _visitors_this -> + let _visitors_r0 = + (fun _visitors_this -> _visitors_this) _visitors_this.variant_id + in + let _visitors_r1 = + self#visit_list + (self#visit_g_typed_value visit_'r visit_'sv visit_'bc visit_'lc) + env _visitors_this.field_values + in + { variant_id = _visitors_r0; field_values = _visitors_r1 } + + method visit_g_typed_value + : 'env 'r_0 'r_1 'sv_0 'sv_1 'bc_0 'bc_1 'lc_0 'lc_1. + ('env -> 'r_0 -> 'r_1) -> + ('env -> 'sv_0 -> 'sv_1) -> + ('env -> 'bc_0 -> 'bc_1) -> + ('env -> 'lc_0 -> 'lc_1) -> + 'env -> + ('r_0, 'sv_0, 'bc_0, 'lc_0) g_typed_value -> + ('r_1, 'sv_1, 'bc_1, 'lc_1) g_typed_value = + fun visit_'r visit_'sv visit_'bc visit_'lc env _visitors_this -> + let _visitors_r0 = + self#visit_g_value visit_'r visit_'sv visit_'bc visit_'lc env + _visitors_this.value + in + let _visitors_r1 = self#visit_ty visit_'r env _visitors_this.ty in + { value = _visitors_r0; ty = _visitors_r1 } + end*) + class ['self] iter_typed_value_base = object (self : 'self) inherit [_] iter_g_typed_value @@ -125,6 +298,18 @@ class ['self] iter_typed_value_base = fun _env _ -> () end +class ['self] map_typed_value_base = + object (self : 'self) + inherit [_] map_g_typed_value + + method visit_erased_region : 'env. 'env -> erased_region -> erased_region = + fun _env r -> r + + method visit_symbolic_proj_comp + : 'env. 'env -> symbolic_proj_comp -> symbolic_proj_comp = + fun _env pc -> pc + end + type value = (erased_region, symbolic_proj_comp, borrow_content, loan_content) g_value (** "Regular" value *) @@ -167,9 +352,29 @@ and typed_value = ancestors = [ "iter_typed_value_base" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); concrete = true; + }, + visitors + { + name = "map_typed_value_incomplete"; + variety = "map"; + ancestors = [ "map_typed_value_base" ]; + nude = true (* Don't inherit [VisitorsRuntime.iter] *); + concrete = true; }] (** "Regular" typed value (we map variables to typed values) *) +(** Override some undefined functions *) +class ['self] map_typed_value = + object (self : 'self) + inherit [_] map_typed_value_incomplete as super + + method! visit_typed_value (env : 'env) (tv : typed_value) : typed_value = + let value = super#visit_value env tv.value in + (* Ignore the type *) + let ty = tv.ty in + { value; ty } + end + type abstract_shared_borrows = | AsbSet of BorrowId.set_t | AsbProjReborrows of symbolic_value * rty @@ -200,6 +405,22 @@ class ['self] iter_typed_avalue_base = fun _env _asb -> () end +class ['self] map_typed_avalue_base = + object (self : 'self) + inherit [_] map_g_typed_value + + method visit_region : 'env. 'env -> region -> region = fun _env r -> r + + method visit_aproj : 'env. 'env -> aproj -> aproj = fun env p -> p + + method visit_typed_value : 'env. 'env -> typed_value -> typed_value = + fun _env v -> v + + method visit_abstract_shared_borrows + : 'env. 'env -> abstract_shared_borrows -> abstract_shared_borrows = + fun _env asb -> asb + end + type avalue = (region, aproj, aborrow_content, aloan_content) g_value (** Abstraction values are used inside of abstractions to properly model borrowing relations introduced by function calls. @@ -238,8 +459,28 @@ and typed_avalue = (region, aproj, aborrow_content, aloan_content) g_typed_value ancestors = [ "iter_typed_avalue_base" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); concrete = true; + }, + visitors + { + name = "map_typed_avalue_incomplete"; + variety = "map"; + ancestors = [ "map_typed_avalue_base" ]; + nude = true (* Don't inherit [VisitorsRuntime.iter] *); + concrete = true; }] +(** Override some undefined functions *) +class ['self] map_typed_avalue = + object (self : 'self) + inherit [_] map_typed_avalue_incomplete as super + + method! visit_typed_avalue (env : 'env) (tv : typed_avalue) : typed_avalue = + let value = super#visit_avalue env tv.value in + (* Ignore the type *) + let ty = tv.ty in + { value; ty } + end + type abs = { abs_id : AbstractionId.id; parents : AbstractionId.set_t; (** The parent abstractions *) |