From 5209cea7012cfa3b39a5a289e65e2ea5e166d730 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 21 Mar 2024 12:34:40 +0100 Subject: WIP: translate.ml and extract.ml do not compile. Some assert left to do and we need to see how translate_crate can give meta to the functions it calls --- compiler/Substitute.ml | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) (limited to 'compiler/Substitute.ml') diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index dbd310b7..a35fdbf3 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -7,6 +7,7 @@ open Types open Values open LlbcAst open Contexts +open Errors (** Generate fresh regions for region variables. @@ -67,25 +68,25 @@ let ctx_adt_get_instantiated_field_types (ctx : eval_ctx) **IMPORTANT**: this function doesn't normalize the types, you may want to use the [AssociatedTypes] equivalent instead. *) -let ctx_adt_value_get_instantiated_field_types (ctx : eval_ctx) +let ctx_adt_value_get_instantiated_field_types (meta : Meta.meta) (ctx : eval_ctx) (adt : adt_value) (id : type_id) (generics : generic_args) : ty list = match id with | TAdtId id -> (* Retrieve the types of the fields *) ctx_adt_get_instantiated_field_types ctx id adt.variant_id generics | TTuple -> - assert (generics.regions = []); + cassert (generics.regions = []) meta "Regions should be empty TODO: error message"; generics.types | TAssumed aty -> ( match aty with | TBox -> - assert (generics.regions = []); - assert (List.length generics.types = 1); - assert (generics.const_generics = []); + cassert (generics.regions = []) meta "Regions should be empty TODO: error message"; + cassert (List.length generics.types = 1) meta "Too many types TODO: error message"; + cassert (generics.const_generics = []) meta "const_generics should be empty TODO: error message"; generics.types | TArray | TSlice | TStr -> (* Those types don't have fields *) - raise (Failure "Unreachable")) + craise meta "Unreachable") (** Substitute a function signature, together with the regions hierarchy associated to that signature. @@ -144,30 +145,30 @@ let subst_ids_visitor (r_subst : RegionId.id -> RegionId.id) method! visit_abstraction_id _ id = asubst id end -let typed_value_subst_ids (r_subst : RegionId.id -> RegionId.id) +let typed_value_subst_ids (meta : Meta.meta) (r_subst : RegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> TypeVarId.id) (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id) (ssubst : SymbolicValueId.id -> SymbolicValueId.id) (bsubst : BorrowId.id -> BorrowId.id) (v : typed_value) : typed_value = - let asubst _ = raise (Failure "Unreachable") in + let asubst _ = craise meta "Unreachable" in let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in vis#visit_typed_value () v -let typed_value_subst_rids (r_subst : RegionId.id -> RegionId.id) +let typed_value_subst_rids (meta : Meta.meta) (r_subst : RegionId.id -> RegionId.id) (v : typed_value) : typed_value = - typed_value_subst_ids r_subst + typed_value_subst_ids meta r_subst (fun x -> x) (fun x -> x) (fun x -> x) (fun x -> x) v -let typed_avalue_subst_ids (r_subst : RegionId.id -> RegionId.id) +let typed_avalue_subst_ids (meta : Meta.meta) (r_subst : RegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> TypeVarId.id) (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id) (ssubst : SymbolicValueId.id -> SymbolicValueId.id) (bsubst : BorrowId.id -> BorrowId.id) (v : typed_avalue) : typed_avalue = - let asubst _ = raise (Failure "Unreachable") in + let asubst _ = craise meta "Unreachable" in let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in vis#visit_typed_avalue () v @@ -189,9 +190,9 @@ let env_subst_ids (r_subst : RegionId.id -> RegionId.id) let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in vis#visit_env () x -let typed_avalue_subst_rids (r_subst : RegionId.id -> RegionId.id) +let typed_avalue_subst_rids (meta : Meta.meta) (r_subst : RegionId.id -> RegionId.id) (x : typed_avalue) : typed_avalue = - let asubst _ = raise (Failure "Unreachable") in + let asubst _ = craise meta "Unreachable" in let vis = subst_ids_visitor r_subst (fun x -> x) -- cgit v1.2.3 From 5ad671a0960692af1c00609fa6864c6f44ca299c Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 28 Mar 2024 13:56:31 +0100 Subject: Should answer all comments, there are still some TODO: error message left --- compiler/Substitute.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'compiler/Substitute.ml') diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index a35fdbf3..14cda863 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -80,9 +80,9 @@ let ctx_adt_value_get_instantiated_field_types (meta : Meta.meta) (ctx : eval_ct | TAssumed aty -> ( match aty with | TBox -> - cassert (generics.regions = []) meta "Regions should be empty TODO: error message"; - cassert (List.length generics.types = 1) meta "Too many types TODO: error message"; - cassert (generics.const_generics = []) meta "const_generics should be empty TODO: error message"; + sanity_check (generics.regions = []) meta; + sanity_check (List.length generics.types = 1) meta; + sanity_check (generics.const_generics = []) meta; generics.types | TArray | TSlice | TStr -> (* Those types don't have fields *) -- cgit v1.2.3 From 64666edb3c10cd42e15937ac4038b83def630e35 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 28 Mar 2024 17:14:27 +0100 Subject: formatting --- compiler/Substitute.ml | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) (limited to 'compiler/Substitute.ml') diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index 14cda863..182dfabf 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -68,14 +68,16 @@ let ctx_adt_get_instantiated_field_types (ctx : eval_ctx) **IMPORTANT**: this function doesn't normalize the types, you may want to use the [AssociatedTypes] equivalent instead. *) -let ctx_adt_value_get_instantiated_field_types (meta : Meta.meta) (ctx : eval_ctx) - (adt : adt_value) (id : type_id) (generics : generic_args) : ty list = +let ctx_adt_value_get_instantiated_field_types (meta : Meta.meta) + (ctx : eval_ctx) (adt : adt_value) (id : type_id) (generics : generic_args) + : ty list = match id with | TAdtId id -> (* Retrieve the types of the fields *) ctx_adt_get_instantiated_field_types ctx id adt.variant_id generics | TTuple -> - cassert (generics.regions = []) meta "Regions should be empty TODO: error message"; + cassert (generics.regions = []) meta + "Regions should be empty TODO: error message"; generics.types | TAssumed aty -> ( match aty with @@ -145,7 +147,8 @@ let subst_ids_visitor (r_subst : RegionId.id -> RegionId.id) method! visit_abstraction_id _ id = asubst id end -let typed_value_subst_ids (meta : Meta.meta) (r_subst : RegionId.id -> RegionId.id) +let typed_value_subst_ids (meta : Meta.meta) + (r_subst : RegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> TypeVarId.id) (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id) (ssubst : SymbolicValueId.id -> SymbolicValueId.id) @@ -154,8 +157,8 @@ let typed_value_subst_ids (meta : Meta.meta) (r_subst : RegionId.id -> RegionId. let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in vis#visit_typed_value () v -let typed_value_subst_rids (meta : Meta.meta) (r_subst : RegionId.id -> RegionId.id) - (v : typed_value) : typed_value = +let typed_value_subst_rids (meta : Meta.meta) + (r_subst : RegionId.id -> RegionId.id) (v : typed_value) : typed_value = typed_value_subst_ids meta r_subst (fun x -> x) (fun x -> x) @@ -163,7 +166,8 @@ let typed_value_subst_rids (meta : Meta.meta) (r_subst : RegionId.id -> RegionId (fun x -> x) v -let typed_avalue_subst_ids (meta : Meta.meta) (r_subst : RegionId.id -> RegionId.id) +let typed_avalue_subst_ids (meta : Meta.meta) + (r_subst : RegionId.id -> RegionId.id) (ty_subst : TypeVarId.id -> TypeVarId.id) (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id) (ssubst : SymbolicValueId.id -> SymbolicValueId.id) @@ -190,8 +194,8 @@ let env_subst_ids (r_subst : RegionId.id -> RegionId.id) let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in vis#visit_env () x -let typed_avalue_subst_rids (meta : Meta.meta) (r_subst : RegionId.id -> RegionId.id) - (x : typed_avalue) : typed_avalue = +let typed_avalue_subst_rids (meta : Meta.meta) + (r_subst : RegionId.id -> RegionId.id) (x : typed_avalue) : typed_avalue = let asubst _ = craise meta "Unreachable" in let vis = subst_ids_visitor r_subst -- cgit v1.2.3 From 786c54c01ea98580374638c0ed92d19dfae19b1f Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 29 Mar 2024 13:21:08 +0100 Subject: added file and line arg to craise and cassert --- compiler/Substitute.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'compiler/Substitute.ml') diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index 182dfabf..b9eebc25 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -76,19 +76,19 @@ let ctx_adt_value_get_instantiated_field_types (meta : Meta.meta) (* Retrieve the types of the fields *) ctx_adt_get_instantiated_field_types ctx id adt.variant_id generics | TTuple -> - cassert (generics.regions = []) meta + cassert __FILE__ __LINE__ (generics.regions = []) meta "Regions should be empty TODO: error message"; generics.types | TAssumed aty -> ( match aty with | TBox -> - sanity_check (generics.regions = []) meta; - sanity_check (List.length generics.types = 1) meta; - sanity_check (generics.const_generics = []) meta; + sanity_check __FILE__ __LINE__ (generics.regions = []) meta; + sanity_check __FILE__ __LINE__ (List.length generics.types = 1) meta; + sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta; generics.types | TArray | TSlice | TStr -> (* Those types don't have fields *) - craise meta "Unreachable") + craise __FILE__ __LINE__ meta "Unreachable") (** Substitute a function signature, together with the regions hierarchy associated to that signature. @@ -153,7 +153,7 @@ let typed_value_subst_ids (meta : Meta.meta) (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id) (ssubst : SymbolicValueId.id -> SymbolicValueId.id) (bsubst : BorrowId.id -> BorrowId.id) (v : typed_value) : typed_value = - let asubst _ = craise meta "Unreachable" in + let asubst _ = craise __FILE__ __LINE__ meta "Unreachable" in let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in vis#visit_typed_value () v @@ -172,7 +172,7 @@ let typed_avalue_subst_ids (meta : Meta.meta) (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id) (ssubst : SymbolicValueId.id -> SymbolicValueId.id) (bsubst : BorrowId.id -> BorrowId.id) (v : typed_avalue) : typed_avalue = - let asubst _ = craise meta "Unreachable" in + let asubst _ = craise __FILE__ __LINE__ meta "Unreachable" in let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in vis#visit_typed_avalue () v @@ -196,7 +196,7 @@ let env_subst_ids (r_subst : RegionId.id -> RegionId.id) let typed_avalue_subst_rids (meta : Meta.meta) (r_subst : RegionId.id -> RegionId.id) (x : typed_avalue) : typed_avalue = - let asubst _ = craise meta "Unreachable" in + let asubst _ = craise __FILE__ __LINE__ meta "Unreachable" in let vis = subst_ids_visitor r_subst (fun x -> x) -- cgit v1.2.3 From 5809c45fbbfcbb78b15a97be619dcde4ab4868b8 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 29 Mar 2024 16:21:15 +0100 Subject: Add some error messages --- compiler/Substitute.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'compiler/Substitute.ml') diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml index b9eebc25..177d8c24 100644 --- a/compiler/Substitute.ml +++ b/compiler/Substitute.ml @@ -77,7 +77,7 @@ let ctx_adt_value_get_instantiated_field_types (meta : Meta.meta) ctx_adt_get_instantiated_field_types ctx id adt.variant_id generics | TTuple -> cassert __FILE__ __LINE__ (generics.regions = []) meta - "Regions should be empty TODO: error message"; + "Tuples don't have region parameters"; generics.types | TAssumed aty -> ( match aty with -- cgit v1.2.3