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/RegionsHierarchy.ml | 31 ++++++++++++++++--------------- 1 file changed, 16 insertions(+), 15 deletions(-) (limited to 'compiler/RegionsHierarchy.ml') diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index 0b589453..4ebdd01a 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -34,23 +34,24 @@ open LlbcAst open LlbcAstUtils open Assumed open SCC +open Errors module Subst = Substitute (** The local logger *) let log = Logging.regions_hierarchy_log -let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) +let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : type_decl TypeDeclId.Map.t) (fun_decls : fun_decl FunDeclId.Map.t) (global_decls : global_decl GlobalDeclId.Map.t) (trait_decls : trait_decl TraitDeclId.Map.t) - (trait_impls : trait_impl TraitImplId.Map.t) (fun_name : string) + (trait_impls : trait_impl TraitImplId.Map.t) (* ?meta *) (fun_name : string) (sg : fun_sig) : region_var_groups = log#ldebug (lazy (__FUNCTION__ ^ ": " ^ fun_name)); (* Initialize a normalization context (we may need to normalize some associated types) *) let norm_ctx : AssociatedTypes.norm_ctx = let norm_trait_types = - AssociatedTypes.compute_norm_trait_types_from_preds + AssociatedTypes.compute_norm_trait_types_from_preds meta sg.preds.trait_type_constraints in { @@ -105,8 +106,8 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) let add_edge ~(short : region) ~(long : region) = (* Sanity checks *) - assert (short <> RErased); - assert (long <> RErased); + cassert_opt_meta (short <> RErased) meta "TODO: Error message"; + cassert_opt_meta (long <> RErased) meta "TODO: Error message"; (* Ignore the locally bound regions (at the level of arrow types for instance *) match (short, long) with | RBVar _, _ | _, RBVar _ -> () @@ -172,13 +173,13 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) | TTraitType (trait_ref, _) -> (* The trait should reference a clause, and not an implementation (otherwise it should have been normalized) *) - assert ( - AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id); + cassert_opt_meta ( + AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id) meta "The trait should reference a clause, and not an implementation (otherwise it should have been normalized)"; (* We have nothing to do *) () | TArrow (regions, inputs, output) -> (* TODO: *) - assert (regions = []); + cassert_opt_meta (regions = []) meta "Regions should be empty"; (* We can ignore the outer regions *) List.iter (explore_ty []) (output :: inputs) and explore_generics (outer : region list) (generics : generic_args) = @@ -221,7 +222,7 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) (SccId.Map.bindings sccs.sccs) in (* The SCC should only contain the 'static *) - assert (static_scc = [ RStatic ]); + cassert_opt_meta (static_scc = [ RStatic ]) meta "The SCC should only contain the 'static"; (* Remove the group as well as references to this group from the other SCCs *) let { sccs; scc_deps } = sccs in @@ -277,7 +278,7 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) (fun r -> match r with | RFVar rid -> RegionId.Map.find rid region_id_to_var_map - | _ -> raise (Failure "Unreachable")) + | _ -> craise (Option.get meta) "Unreachable") scc in @@ -317,19 +318,19 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t) let regular = List.map (fun ((fid, d) : FunDeclId.id * fun_decl) -> - (FRegular fid, (Types.name_to_string env d.name, d.signature))) + (FRegular fid, (Types.name_to_string env d.name, d.signature, Some d.meta))) (FunDeclId.Map.bindings fun_decls) in let assumed = List.map (fun (info : assumed_fun_info) -> - (FAssumed info.fun_id, (info.name, info.fun_sig))) + (FAssumed info.fun_id, (info.name, info.fun_sig, None))) assumed_fun_infos in FunIdMap.of_list (List.map - (fun (fid, (name, sg)) -> + (fun (fid, (name, sg, meta)) -> ( fid, - compute_regions_hierarchy_for_sig type_decls fun_decls global_decls - trait_decls trait_impls name sg )) + compute_regions_hierarchy_for_sig meta type_decls fun_decls global_decls + trait_decls trait_impls name sg)) (regular @ assumed)) -- cgit v1.2.3 From 7a304e990d80dc052f63f66401544040fa0f2728 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Tue, 26 Mar 2024 12:14:32 +0100 Subject: added a meta option field to norm_ctx and changed the meta used by some assert to the norm_ctx one --- compiler/RegionsHierarchy.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'compiler/RegionsHierarchy.ml') diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index 4ebdd01a..0672a25f 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -55,6 +55,7 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : ty sg.preds.trait_type_constraints in { + meta = meta; norm_trait_types; type_decls; fun_decls; -- cgit v1.2.3 From 0f0082c81db8852dff23cd4691af19c434c8be78 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Wed, 27 Mar 2024 10:22:06 +0100 Subject: Added sanity_check and sanity_check_opt_meta helpers and changed sanity checks related cassert to these helpers to have a proper error message --- compiler/RegionsHierarchy.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'compiler/RegionsHierarchy.ml') diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index 0672a25f..f4e2ff35 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -107,8 +107,8 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : ty let add_edge ~(short : region) ~(long : region) = (* Sanity checks *) - cassert_opt_meta (short <> RErased) meta "TODO: Error message"; - cassert_opt_meta (long <> RErased) meta "TODO: Error message"; + sanity_check_opt_meta (short <> RErased) meta; + sanity_check_opt_meta (long <> RErased) meta; (* Ignore the locally bound regions (at the level of arrow types for instance *) match (short, long) with | RBVar _, _ | _, RBVar _ -> () -- 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/RegionsHierarchy.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'compiler/RegionsHierarchy.ml') diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index f4e2ff35..a4d66854 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -44,7 +44,7 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : ty (fun_decls : fun_decl FunDeclId.Map.t) (global_decls : global_decl GlobalDeclId.Map.t) (trait_decls : trait_decl TraitDeclId.Map.t) - (trait_impls : trait_impl TraitImplId.Map.t) (* ?meta *) (fun_name : string) + (trait_impls : trait_impl TraitImplId.Map.t) (fun_name : string) (sg : fun_sig) : region_var_groups = log#ldebug (lazy (__FUNCTION__ ^ ": " ^ fun_name)); (* Initialize a normalization context (we may need to normalize some @@ -174,13 +174,13 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : ty | TTraitType (trait_ref, _) -> (* The trait should reference a clause, and not an implementation (otherwise it should have been normalized) *) - cassert_opt_meta ( - AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id) meta "The trait should reference a clause, and not an implementation (otherwise it should have been normalized)"; + sanity_check_opt_meta ( + AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id) meta; (* We have nothing to do *) () | TArrow (regions, inputs, output) -> (* TODO: *) - cassert_opt_meta (regions = []) meta "Regions should be empty"; + cassert_opt_meta (regions = []) meta "We don't support arrow types with locally quantified regions"; (* We can ignore the outer regions *) List.iter (explore_ty []) (output :: inputs) and explore_generics (outer : region list) (generics : generic_args) = @@ -223,7 +223,7 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : ty (SccId.Map.bindings sccs.sccs) in (* The SCC should only contain the 'static *) - cassert_opt_meta (static_scc = [ RStatic ]) meta "The SCC should only contain the 'static"; + sanity_check_opt_meta (static_scc = [ RStatic ]) meta; (* Remove the group as well as references to this group from the other SCCs *) let { sccs; scc_deps } = sccs in -- 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/RegionsHierarchy.ml | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) (limited to 'compiler/RegionsHierarchy.ml') diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index a4d66854..7267dd3d 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -40,7 +40,8 @@ module Subst = Substitute (** The local logger *) let log = Logging.regions_hierarchy_log -let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : type_decl TypeDeclId.Map.t) +let compute_regions_hierarchy_for_sig (meta : Meta.meta option) + (type_decls : type_decl TypeDeclId.Map.t) (fun_decls : fun_decl FunDeclId.Map.t) (global_decls : global_decl GlobalDeclId.Map.t) (trait_decls : trait_decl TraitDeclId.Map.t) @@ -51,11 +52,11 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : ty associated types) *) let norm_ctx : AssociatedTypes.norm_ctx = let norm_trait_types = - AssociatedTypes.compute_norm_trait_types_from_preds meta + AssociatedTypes.compute_norm_trait_types_from_preds meta sg.preds.trait_type_constraints in { - meta = meta; + meta; norm_trait_types; type_decls; fun_decls; @@ -174,13 +175,15 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (type_decls : ty | TTraitType (trait_ref, _) -> (* The trait should reference a clause, and not an implementation (otherwise it should have been normalized) *) - sanity_check_opt_meta ( - AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id) meta; + sanity_check_opt_meta + (AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id) + meta; (* We have nothing to do *) () | TArrow (regions, inputs, output) -> (* TODO: *) - cassert_opt_meta (regions = []) meta "We don't support arrow types with locally quantified regions"; + cassert_opt_meta (regions = []) meta + "We don't support arrow types with locally quantified regions"; (* We can ignore the outer regions *) List.iter (explore_ty []) (output :: inputs) and explore_generics (outer : region list) (generics : generic_args) = @@ -319,7 +322,8 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t) let regular = List.map (fun ((fid, d) : FunDeclId.id * fun_decl) -> - (FRegular fid, (Types.name_to_string env d.name, d.signature, Some d.meta))) + ( FRegular fid, + (Types.name_to_string env d.name, d.signature, Some d.meta) )) (FunDeclId.Map.bindings fun_decls) in let assumed = @@ -332,6 +336,6 @@ let compute_regions_hierarchies (type_decls : type_decl TypeDeclId.Map.t) (List.map (fun (fid, (name, sg, meta)) -> ( fid, - compute_regions_hierarchy_for_sig meta type_decls fun_decls global_decls - trait_decls trait_impls name sg)) + compute_regions_hierarchy_for_sig meta type_decls fun_decls + global_decls trait_decls trait_impls name sg )) (regular @ assumed)) -- 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/RegionsHierarchy.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'compiler/RegionsHierarchy.ml') diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index 7267dd3d..713cdef9 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -108,8 +108,8 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) let add_edge ~(short : region) ~(long : region) = (* Sanity checks *) - sanity_check_opt_meta (short <> RErased) meta; - sanity_check_opt_meta (long <> RErased) meta; + sanity_check_opt_meta __FILE__ __LINE__ (short <> RErased) meta; + sanity_check_opt_meta __FILE__ __LINE__ (long <> RErased) meta; (* Ignore the locally bound regions (at the level of arrow types for instance *) match (short, long) with | RBVar _, _ | _, RBVar _ -> () @@ -175,14 +175,14 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) | TTraitType (trait_ref, _) -> (* The trait should reference a clause, and not an implementation (otherwise it should have been normalized) *) - sanity_check_opt_meta + sanity_check_opt_meta __FILE__ __LINE__ (AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id) meta; (* We have nothing to do *) () | TArrow (regions, inputs, output) -> (* TODO: *) - cassert_opt_meta (regions = []) meta + cassert_opt_meta __FILE__ __LINE__ (regions = []) meta "We don't support arrow types with locally quantified regions"; (* We can ignore the outer regions *) List.iter (explore_ty []) (output :: inputs) @@ -226,7 +226,7 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (SccId.Map.bindings sccs.sccs) in (* The SCC should only contain the 'static *) - sanity_check_opt_meta (static_scc = [ RStatic ]) meta; + sanity_check_opt_meta __FILE__ __LINE__ (static_scc = [ RStatic ]) meta; (* Remove the group as well as references to this group from the other SCCs *) let { sccs; scc_deps } = sccs in @@ -282,7 +282,7 @@ let compute_regions_hierarchy_for_sig (meta : Meta.meta option) (fun r -> match r with | RFVar rid -> RegionId.Map.find rid region_id_to_var_map - | _ -> craise (Option.get meta) "Unreachable") + | _ -> craise __FILE__ __LINE__ (Option.get meta) "Unreachable") scc in -- cgit v1.2.3