From 09f51ecbe70f64168143dc489ad1e413a9aab41c Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 16 Oct 2024 14:23:13 -0700 Subject: [PATCH] remove linear lookup of lids in gamma_sig --- .../generated/FStarC_TypeChecker_Env.ml | 91 +++---------------- src/typechecker/FStarC.TypeChecker.Env.fst | 38 ++------ 2 files changed, 23 insertions(+), 106 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Env.ml index 00c47d6e62d..f8d34157341 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Env.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Env.ml @@ -2946,72 +2946,20 @@ let (lookup_qname : env -> FStarC_Ident.lident -> qninfo) = FStarC_Compiler_Util.smap_try_find (gamma_cache env1) uu___1 in match uu___ with | FStar_Pervasives_Native.None -> - let uu___1 = - FStarC_Compiler_Util.find_map env1.gamma - (fun uu___2 -> - match uu___2 with - | FStarC_Syntax_Syntax.Binding_lid (l, (us_names, t)) - when FStarC_Ident.lid_equals lid l -> - let us = - FStarC_Compiler_List.map - (fun uu___3 -> - FStarC_Syntax_Syntax.U_name uu___3) us_names in - let uu___3 = - let uu___4 = FStarC_Ident.range_of_lid l in - ((FStar_Pervasives.Inl (us, t)), uu___4) in - FStar_Pervasives_Native.Some uu___3 - | uu___3 -> FStar_Pervasives_Native.None) in - FStarC_Compiler_Util.catch_opt uu___1 - (fun uu___2 -> - FStarC_Compiler_Util.find_map env1.gamma_sig - (fun uu___3 -> - match uu___3 with - | (uu___4, - { - FStarC_Syntax_Syntax.sigel = - FStarC_Syntax_Syntax.Sig_bundle - { FStarC_Syntax_Syntax.ses = ses; - FStarC_Syntax_Syntax.lids = uu___5;_}; - FStarC_Syntax_Syntax.sigrng = uu___6; - FStarC_Syntax_Syntax.sigquals = uu___7; - FStarC_Syntax_Syntax.sigmeta = uu___8; - FStarC_Syntax_Syntax.sigattrs = uu___9; - FStarC_Syntax_Syntax.sigopens_and_abbrevs = - uu___10; - FStarC_Syntax_Syntax.sigopts = uu___11;_}) - -> - FStarC_Compiler_Util.find_map ses - (fun se -> - let uu___12 = - FStarC_Compiler_Util.for_some - (FStarC_Ident.lid_equals lid) - (FStarC_Syntax_Util.lids_of_sigelt se) in - if uu___12 - then - cache - ((FStar_Pervasives.Inr - (se, FStar_Pervasives_Native.None)), - (FStarC_Syntax_Util.range_of_sigelt se)) - else FStar_Pervasives_Native.None) - | (lids, s) -> - let maybe_cache t = - match s.FStarC_Syntax_Syntax.sigel with - | FStarC_Syntax_Syntax.Sig_declare_typ uu___4 - -> FStar_Pervasives_Native.Some t - | uu___4 -> cache t in - let uu___4 = - FStarC_Compiler_List.tryFind - (FStarC_Ident.lid_equals lid) lids in - (match uu___4 with - | FStar_Pervasives_Native.None -> - FStar_Pervasives_Native.None - | FStar_Pervasives_Native.Some l -> - let uu___5 = - let uu___6 = FStarC_Ident.range_of_lid l in - ((FStar_Pervasives.Inr - (s, FStar_Pervasives_Native.None)), - uu___6) in - maybe_cache uu___5))) + FStarC_Compiler_Util.find_map env1.gamma + (fun uu___1 -> + match uu___1 with + | FStarC_Syntax_Syntax.Binding_lid (l, (us_names, t)) when + FStarC_Ident.lid_equals lid l -> + let us = + FStarC_Compiler_List.map + (fun uu___2 -> FStarC_Syntax_Syntax.U_name uu___2) + us_names in + let uu___2 = + let uu___3 = FStarC_Ident.range_of_lid l in + ((FStar_Pervasives.Inl (us, t)), uu___3) in + FStar_Pervasives_Native.Some uu___2 + | uu___2 -> FStar_Pervasives_Native.None) | se -> se else FStar_Pervasives_Native.None in if FStarC_Compiler_Util.is_some found @@ -6503,17 +6451,6 @@ let (finish_module : env -> FStarC_Syntax_Syntax.modul -> env) = FStarC_Ident.lid_of_ids uu___ in fun env1 -> fun m -> - let sigs = - let uu___ = - FStarC_Ident.lid_equals m.FStarC_Syntax_Syntax.name - FStarC_Parser_Const.prims_lid in - if uu___ - then - let uu___1 = - FStarC_Compiler_List.map FStar_Pervasives_Native.snd - env1.gamma_sig in - FStarC_Compiler_List.rev uu___1 - else m.FStarC_Syntax_Syntax.declarations in { solver = (env1.solver); range = (env1.range); diff --git a/src/typechecker/FStarC.TypeChecker.Env.fst b/src/typechecker/FStarC.TypeChecker.Env.fst index 44f78f7c3a2..a8ebf4d6dd9 100644 --- a/src/typechecker/FStarC.TypeChecker.Env.fst +++ b/src/typechecker/FStarC.TypeChecker.Env.fst @@ -460,31 +460,15 @@ let lookup_qname env (lid:lident) : qninfo = if cur_mod <> No then match BU.smap_try_find (gamma_cache env) (string_of_lid lid) with | None -> - BU.catch_opt - (BU.find_map env.gamma (function - | Binding_lid(l, (us_names, t)) when lid_equals lid l-> - (* A recursive definition. - * We must return the exact set of universes on which - * it is being defined, and not instantiate it. - * TODO: could we cache this? *) - let us = List.map U_name us_names in - Some (Inl (us, t), Ident.range_of_lid l) - | _ -> None)) - (fun () -> BU.find_map env.gamma_sig (function - | (_, { sigel = Sig_bundle {ses} }) -> - BU.find_map ses (fun se -> - if lids_of_sigelt se |> BU.for_some (lid_equals lid) - then cache (Inr (se, None), U.range_of_sigelt se) - else None) - | (lids, s) -> - let maybe_cache t = match s.sigel with - | Sig_declare_typ _ -> Some t - | _ -> cache t - in - begin match List.tryFind (lid_equals lid) lids with - | None -> None - | Some l -> maybe_cache (Inr (s, None), Ident.range_of_lid l) - end)) + (BU.find_map env.gamma (function + | Binding_lid(l, (us_names, t)) when lid_equals lid l-> + (* A recursive definition. + * We must return the exact set of universes on which + * it is being defined, and not instantiate it. + * TODO: could we cache this? *) + let us = List.map U_name us_names in + Some (Inl (us, t), Ident.range_of_lid l) + | _ -> None)) | se -> se else None in @@ -1791,10 +1775,6 @@ let clear_expected_typ (env_: env): env & option (typ & bool) = let finish_module = let empty_lid = lid_of_ids [id_of_text ""] in fun env m -> - let sigs = - if lid_equals m.name Const.prims_lid - then env.gamma_sig |> List.map snd |> List.rev - else m.declarations in {env with curmodule=empty_lid; gamma=[];