From 6f22190cba92a44b6c74bfcce8f5ed142a68e195 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 31 Aug 2023 12:47:43 +0200 Subject: Start adding support for traits --- compiler/InterpreterPaths.mli | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'compiler/InterpreterPaths.mli') diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli index 4a9f3b41..041b0a97 100644 --- a/compiler/InterpreterPaths.mli +++ b/compiler/InterpreterPaths.mli @@ -3,6 +3,7 @@ module V = Values module E = Expressions module C = Contexts module Subst = Substitute +module Assoc = AssociatedTypes module L = Logging open Cps open InterpreterExpansion @@ -56,12 +57,10 @@ val compute_expanded_bottom_tuple_value : T.ety list -> V.typed_value (** Compute an expanded ADT ⊥ value *) val compute_expanded_bottom_adt_value : - T.type_decl T.TypeDeclId.Map.t -> + C.eval_ctx -> T.TypeDeclId.id -> T.VariantId.id option -> - T.erased_region list -> - T.ety list -> - T.const_generic list -> + T.egeneric_args -> V.typed_value (** Compute an expanded [Option] ⊥ value *) -- cgit v1.2.3 From 838cc86cb2efc8fb64a94a94b58b82d66844e7e4 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 23 Oct 2023 13:47:39 +0200 Subject: Remove some assumed types and add more support for builtin definitions --- compiler/InterpreterPaths.mli | 4 ---- 1 file changed, 4 deletions(-) (limited to 'compiler/InterpreterPaths.mli') diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli index 041b0a97..0ff8063f 100644 --- a/compiler/InterpreterPaths.mli +++ b/compiler/InterpreterPaths.mli @@ -63,10 +63,6 @@ val compute_expanded_bottom_adt_value : T.egeneric_args -> V.typed_value -(** Compute an expanded [Option] ⊥ value *) -val compute_expanded_bottom_option_value : - T.VariantId.id -> T.ety -> V.typed_value - (** Drop (end) outer loans at a given place, which should be seen as an l-value (we will write to it later, but need to drop the loans before writing). -- cgit v1.2.3 From b9f33bdd871a1bd7a1bd29f148dd05bd7990548b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 19:28:56 +0100 Subject: Remove the 'r type variable from the ty type definition --- compiler/InterpreterPaths.mli | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'compiler/InterpreterPaths.mli') diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli index 0ff8063f..a493ad69 100644 --- a/compiler/InterpreterPaths.mli +++ b/compiler/InterpreterPaths.mli @@ -55,12 +55,15 @@ val write_place : *) val compute_expanded_bottom_tuple_value : T.ety list -> V.typed_value -(** Compute an expanded ADT ⊥ value *) +(** Compute an expanded ADT ⊥ value. + + The types in the generics should use erased regions. + *) val compute_expanded_bottom_adt_value : C.eval_ctx -> T.TypeDeclId.id -> T.VariantId.id option -> - T.egeneric_args -> + T.generic_args -> V.typed_value (** Drop (end) outer loans at a given place, which should be seen as an l-value -- cgit v1.2.3 From 21e3b719f2338f4d4a65c91edc0eb83d0b22393e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 15 Nov 2023 22:03:21 +0100 Subject: Start updating the name type, cleanup the names and the module abbrevs --- compiler/InterpreterPaths.mli | 40 +++++++++++++++++----------------------- 1 file changed, 17 insertions(+), 23 deletions(-) (limited to 'compiler/InterpreterPaths.mli') diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli index a493ad69..3e29b810 100644 --- a/compiler/InterpreterPaths.mli +++ b/compiler/InterpreterPaths.mli @@ -1,13 +1,8 @@ -module T = Types -module V = Values -module E = Expressions -module C = Contexts -module Subst = Substitute -module Assoc = AssociatedTypes -module L = Logging +open Types +open Values +open Expressions +open Contexts open Cps -open InterpreterExpansion -module Synth = SynthesizeSymbolic type access_kind = Read | Write | Move @@ -18,13 +13,13 @@ type access_kind = Read | Write | Move updates the environment (by ending borrows, expanding symbolic values, etc.) until it manages to fully access the provided place. *) -val update_ctx_along_read_place : C.config -> access_kind -> E.place -> cm_fun +val update_ctx_along_read_place : config -> access_kind -> place -> cm_fun (** Update the environment to be able to write to a place. See {!update_ctx_along_read_place}. *) -val update_ctx_along_write_place : C.config -> access_kind -> E.place -> cm_fun +val update_ctx_along_write_place : config -> access_kind -> place -> cm_fun (** Read the value at a given place. @@ -34,7 +29,7 @@ val update_ctx_along_write_place : C.config -> access_kind -> E.place -> cm_fun Note that we only access the value at the place, and do not check that the value is "well-formed" (for instance that it doesn't contain bottoms). *) -val read_place : access_kind -> E.place -> C.eval_ctx -> V.typed_value +val read_place : access_kind -> place -> eval_ctx -> typed_value (** Update the value at a given place. @@ -45,26 +40,25 @@ val read_place : access_kind -> E.place -> C.eval_ctx -> V.typed_value the overwritten value contains borrows, loans, etc. and will simply overwrite it. *) -val write_place : - access_kind -> E.place -> V.typed_value -> C.eval_ctx -> C.eval_ctx +val write_place : access_kind -> place -> typed_value -> eval_ctx -> eval_ctx (** Compute an expanded tuple ⊥ value. [compute_expanded_bottom_tuple_value [ty0, ..., tyn]] returns [(⊥:ty0, ..., ⊥:tyn)] *) -val compute_expanded_bottom_tuple_value : T.ety list -> V.typed_value +val compute_expanded_bottom_tuple_value : ety list -> typed_value (** Compute an expanded ADT ⊥ value. The types in the generics should use erased regions. *) val compute_expanded_bottom_adt_value : - C.eval_ctx -> - T.TypeDeclId.id -> - T.VariantId.id option -> - T.generic_args -> - V.typed_value + eval_ctx -> + TypeDeclId.id -> + VariantId.id option -> + generic_args -> + typed_value (** Drop (end) outer loans at a given place, which should be seen as an l-value (we will write to it later, but need to drop the loans before writing). @@ -79,7 +73,7 @@ val compute_expanded_bottom_adt_value : that the place is *inside* a borrow, if we end the borrow, we won't be able to reinsert the value back). *) -val drop_outer_loans_at_lplace : C.config -> E.place -> cm_fun +val drop_outer_loans_at_lplace : config -> place -> cm_fun (** End the loans at a given place: read the value, if it contains a loan, end this loan, repeat. @@ -90,7 +84,7 @@ val drop_outer_loans_at_lplace : C.config -> E.place -> cm_fun when moving values, we can't move a value which contains loans and thus need to end them, etc. *) -val end_loans_at_place : C.config -> access_kind -> E.place -> cm_fun +val end_loans_at_place : config -> access_kind -> place -> cm_fun (** Small utility. @@ -101,4 +95,4 @@ val end_loans_at_place : C.config -> access_kind -> E.place -> cm_fun place. This value should not contain any outer loan (and we check it is the case). Note that this value is very likely to contain ⊥ subvalues. *) -val prepare_lplace : C.config -> E.place -> (V.typed_value -> m_fun) -> m_fun +val prepare_lplace : config -> place -> (typed_value -> m_fun) -> m_fun -- cgit v1.2.3