diff --git a/charon-ml/src/NameMatcher.ml b/charon-ml/src/NameMatcher.ml index fb534568..9062044d 100644 --- a/charon-ml/src/NameMatcher.ml +++ b/charon-ml/src/NameMatcher.ml @@ -235,8 +235,7 @@ let ctx_to_fmt_env (ctx : ctx) : PrintLlbcAst.fmt_env = global_decls = ctx.global_decls; trait_decls = ctx.trait_decls; trait_impls = ctx.trait_impls; - regions = []; - generics = TypesUtils.empty_generic_params; + generics = []; locals = []; } diff --git a/charon-ml/src/PrintLlbcAst.ml b/charon-ml/src/PrintLlbcAst.ml index ada4838b..02319463 100644 --- a/charon-ml/src/PrintLlbcAst.ml +++ b/charon-ml/src/PrintLlbcAst.ml @@ -150,8 +150,7 @@ module Crate = struct global_decls = m.global_decls; trait_decls = m.trait_decls; trait_impls = m.trait_impls; - regions = []; - generics = empty_generic_params; + generics = []; locals = []; } diff --git a/charon-ml/src/PrintTypes.ml b/charon-ml/src/PrintTypes.ml index 11534fb1..1caff170 100644 --- a/charon-ml/src/PrintTypes.ml +++ b/charon-ml/src/PrintTypes.ml @@ -7,9 +7,6 @@ open TypesUtils open GAst open PrintUtils -let type_var_to_string (tv : type_var) : string = tv.name -let const_generic_var_to_string (v : const_generic_var) : string = v.name - let region_var_to_string (rv : region_var) : string = match rv.name with | Some name -> name @@ -22,23 +19,39 @@ let ref_kind_to_string (rk : ref_kind) : string = let builtin_ty_to_string (_ : builtin_ty) : string = "Box" -let trait_clause_id_to_pretty_string (id : trait_clause_id) : string = - "TraitClause@" ^ TraitClauseId.to_string id - -let de_bruijn_var_to_pretty_string show_bound show_free var : string = +let de_bruijn_var_to_pretty_string show_varid var : string = match var with - | Bound (dbid, varid) -> show_de_bruijn_id dbid ^ "_" ^ show_bound varid - | Free varid -> "'" ^ show_free varid + | Bound (dbid, varid) -> show_de_bruijn_id dbid ^ "_" ^ show_varid varid + | Free varid -> show_varid varid let region_db_var_to_pretty_string (var : region_db_var) : string = - "'" ^ de_bruijn_var_to_pretty_string RegionId.to_string RegionId.to_string var + "'" ^ de_bruijn_var_to_pretty_string RegionId.to_string var + +let type_db_var_to_pretty_string (var : type_db_var) : string = + "T@" ^ de_bruijn_var_to_pretty_string TypeVarId.to_string var let type_var_id_to_pretty_string (id : type_var_id) : string = "T@" ^ TypeVarId.to_string id +let type_var_to_string (tv : type_var) : string = tv.name + let const_generic_var_id_to_pretty_string (id : const_generic_var_id) : string = "C@" ^ ConstGenericVarId.to_string id +let const_generic_db_var_to_pretty_string (var : const_generic_db_var) : string + = + "C@" ^ de_bruijn_var_to_pretty_string ConstGenericVarId.to_string var + +let const_generic_var_to_string (v : const_generic_var) : string = v.name + +let trait_clause_id_to_pretty_string (id : trait_clause_id) : string = + "TraitClause@" ^ TraitClauseId.to_string id + +let trait_db_var_to_pretty_string (var : trait_db_var) : string = + "TraitClause@" ^ de_bruijn_var_to_pretty_string TraitClauseId.to_string var + +let trait_clause_id_to_string _ id = trait_clause_id_to_pretty_string id + let type_decl_id_to_pretty_string (id : type_decl_id) : string = "TypeDecl@" ^ TypeDeclId.to_string id @@ -60,57 +73,64 @@ let variant_id_to_pretty_string (id : variant_id) : string = let field_id_to_pretty_string (id : field_id) : string = "Field@" ^ FieldId.to_string id -let trait_clause_id_to_string _ id = trait_clause_id_to_pretty_string id +let lookup_var_in_env (env : 'a fmt_env) + (find_in : generic_params -> 'id -> 'b option) (var : 'id de_bruijn_var) : + 'b option = + if List.length env.generics == 0 then None + else + let dbid, varid = + match var with + | Bound (dbid, varid) -> (dbid, varid) + | Free varid -> + let len = List.length env.generics in + let dbid = len - 1 in + (dbid, varid) + in + match List.nth_opt env.generics dbid with + | None -> None + | Some generics -> begin + match find_in generics varid with + | None -> None + | Some r -> Some r + end let region_db_var_to_string (env : 'a fmt_env) (var : region_db_var) : string = - let dbid, varid = - match var with - | Bound (dbid, varid) -> (dbid, varid) - | Free varid -> - let len = List.length env.regions in - let dbid = if len == 0 then 0 else len - 1 in - (dbid, varid) + (* Note that the regions are not necessarily ordered following their indices *) + let find (generics : generic_params) varid = + List.find_opt (fun (v : region_var) -> v.index = varid) generics.regions in - match List.nth_opt env.regions dbid with + match lookup_var_in_env env find var with | None -> region_db_var_to_pretty_string var - | Some regions -> begin - (* Note that the regions are not necessarily ordered following their indices *) - match List.find_opt (fun (r : region_var) -> r.index = varid) regions with - | None -> region_db_var_to_pretty_string var - | Some r -> region_var_to_string r - end + | Some r -> region_var_to_string r let type_db_var_to_string (env : 'a fmt_env) (var : type_db_var) : string = - match var with - | Bound _ -> failwith "bound type variable" - | Free id -> begin - (* Note that the types are not necessarily ordered following their indices *) - match - List.find_opt (fun (x : type_var) -> x.index = id) env.generics.types - with - | None -> type_var_id_to_pretty_string id - | Some x -> type_var_to_string x - end + let find (generics : generic_params) varid = + List.find_opt (fun (v : type_var) -> v.index = varid) generics.types + in + match lookup_var_in_env env find var with + | None -> type_db_var_to_pretty_string var + | Some r -> type_var_to_string r let const_generic_db_var_to_string (env : 'a fmt_env) (var : const_generic_db_var) : string = - match var with - | Bound _ -> failwith "bound const generic variable" - | Free id -> begin - (* Note that the types are not necessarily ordered following their indices *) - match - List.find_opt - (fun (x : const_generic_var) -> x.index = id) - env.generics.const_generics - with - | None -> const_generic_var_id_to_pretty_string id - | Some x -> const_generic_var_to_string x - end + let find (generics : generic_params) varid = + List.find_opt + (fun (v : const_generic_var) -> v.index = varid) + generics.const_generics + in + match lookup_var_in_env env find var with + | None -> const_generic_db_var_to_pretty_string var + | Some r -> const_generic_var_to_string r let trait_db_var_to_string (env : 'a fmt_env) (var : trait_db_var) : string = - match var with - | Bound _ -> failwith "bound trait clause variable" - | Free id -> trait_clause_id_to_pretty_string id + let find (generics : generic_params) varid = + List.find_opt + (fun (v : trait_clause) -> v.clause_id = varid) + generics.trait_clauses + in + match lookup_var_in_env env find var with + | None -> trait_db_var_to_pretty_string var + | Some r -> trait_clause_id_to_pretty_string r.clause_id let region_to_string (env : 'a fmt_env) (r : region) : string = match r with @@ -205,7 +225,7 @@ and ty_to_string (env : 'a fmt_env) (ty : ty) : string = | RMut -> "*mut " ^ ty_to_string env rty | RShared -> "*const " ^ ty_to_string env rty) | TArrow binder -> - let env = { env with regions = binder.binder_regions :: env.regions } in + let env = fmt_env_push_regions env binder.binder_regions in let inputs, output = binder.binder_value in let inputs = "(" ^ String.concat ", " (List.map (ty_to_string env) inputs) ^ ") -> " diff --git a/charon-ml/src/PrintUllbcAst.ml b/charon-ml/src/PrintUllbcAst.ml index ff8acb88..de755467 100644 --- a/charon-ml/src/PrintUllbcAst.ml +++ b/charon-ml/src/PrintUllbcAst.ml @@ -119,8 +119,7 @@ module Crate = struct global_decls = m.global_decls; trait_decls = m.trait_decls; trait_impls = m.trait_impls; - regions = []; - generics = empty_generic_params; + generics = []; locals = []; } in diff --git a/charon-ml/src/PrintUtils.ml b/charon-ml/src/PrintUtils.ml index 70e65106..ef51d146 100644 --- a/charon-ml/src/PrintUtils.ml +++ b/charon-ml/src/PrintUtils.ml @@ -19,26 +19,21 @@ type 'fun_body fmt_env = { global_decls : global_decl GlobalDeclId.Map.t; trait_decls : trait_decl TraitDeclId.Map.t; trait_impls : trait_impl TraitImplId.Map.t; - regions : region_var list list; - (** We have a stack of regions, because we can dive into groups of - universally quantified regions (for instance because of the arrow - type). - - Note that the variables in the generics don't need to be ordered following their - indices, i.e., the region var of index 0 doesn't have to be at index 0, - etc. We lookup the variables by checking their id, not their position. + generics : generic_params list; + (** We have a stack of generic parameters, because we can dive into + binders (for instance because of the arrow type). *) - generics : generic_params; - (* We ignore `generics.regions` as they are tracked in `regions` already *) locals : (VarId.id * string option) list; (** The local variables don't need to be ordered (same as the generics) *) } let fmt_env_update_generics_and_preds (env : 'a fmt_env) (generics : generic_params) : 'a fmt_env = - let { regions; _ } : generic_params = generics in - { env with regions = regions :: env.regions; generics } + { env with generics = generics :: env.generics } let fmt_env_push_regions (env : 'a fmt_env) (regions : region_var list) : 'a fmt_env = - { env with regions = regions :: env.regions } + { + env with + generics = { TypesUtils.empty_generic_params with regions } :: env.generics; + }