diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_DsEnv.ml b/ocaml/fstar-lib/generated/FStar_Syntax_DsEnv.ml index 479be57fc5a..b25d7b10eee 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_DsEnv.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_DsEnv.ml @@ -127,12 +127,7 @@ type env = (FStar_Ident.lident * FStar_Parser_AST.decl Prims.list) Prims.list ; syntax_only: Prims.bool ; ds_hooks: dsenv_hooks ; - dep_graph: FStar_Parser_Dep.deps ; - opens_and_abbrevs_of: - (FStar_Syntax_Syntax.open_module_or_namespace, - FStar_Syntax_Syntax.module_abbrev) FStar_Pervasives.either Prims.list - FStar_Compiler_Util.smap - } + dep_graph: FStar_Parser_Dep.deps } and dsenv_hooks = { ds_push_open_hook: @@ -147,7 +142,7 @@ let (__proj__Mkenv__item__curmodule : | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> curmodule + ds_hooks; dep_graph;_} -> curmodule let (__proj__Mkenv__item__curmonad : env -> FStar_Ident.ident FStar_Pervasives_Native.option) = fun projectee -> @@ -155,7 +150,7 @@ let (__proj__Mkenv__item__curmonad : | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> curmonad + ds_hooks; dep_graph;_} -> curmonad let (__proj__Mkenv__item__modules : env -> (FStar_Ident.lident * FStar_Syntax_Syntax.modul) Prims.list) = fun projectee -> @@ -163,14 +158,14 @@ let (__proj__Mkenv__item__modules : | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> modules + ds_hooks; dep_graph;_} -> modules let (__proj__Mkenv__item__scope_mods : env -> scope_mod Prims.list) = fun projectee -> match projectee with | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> scope_mods + ds_hooks; dep_graph;_} -> scope_mods let (__proj__Mkenv__item__exported_ids : env -> exported_id_set FStar_Compiler_Util.smap) = fun projectee -> @@ -178,7 +173,7 @@ let (__proj__Mkenv__item__exported_ids : | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> exported_ids + ds_hooks; dep_graph;_} -> exported_ids let (__proj__Mkenv__item__trans_exported_ids : env -> exported_id_set FStar_Compiler_Util.smap) = fun projectee -> @@ -186,7 +181,7 @@ let (__proj__Mkenv__item__trans_exported_ids : | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> trans_exported_ids + ds_hooks; dep_graph;_} -> trans_exported_ids let (__proj__Mkenv__item__includes : env -> (FStar_Ident.lident * FStar_Syntax_Syntax.restriction) Prims.list @@ -197,14 +192,14 @@ let (__proj__Mkenv__item__includes : | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> includes + ds_hooks; dep_graph;_} -> includes let (__proj__Mkenv__item__sigaccum : env -> FStar_Syntax_Syntax.sigelts) = fun projectee -> match projectee with | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> sigaccum + ds_hooks; dep_graph;_} -> sigaccum let (__proj__Mkenv__item__sigmap : env -> (FStar_Syntax_Syntax.sigelt * Prims.bool) FStar_Compiler_Util.smap) = @@ -213,28 +208,28 @@ let (__proj__Mkenv__item__sigmap : | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> sigmap + ds_hooks; dep_graph;_} -> sigmap let (__proj__Mkenv__item__iface : env -> Prims.bool) = fun projectee -> match projectee with | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> iface + ds_hooks; dep_graph;_} -> iface let (__proj__Mkenv__item__admitted_iface : env -> Prims.bool) = fun projectee -> match projectee with | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> admitted_iface + ds_hooks; dep_graph;_} -> admitted_iface let (__proj__Mkenv__item__expect_typ : env -> Prims.bool) = fun projectee -> match projectee with | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> expect_typ + ds_hooks; dep_graph;_} -> expect_typ let (__proj__Mkenv__item__remaining_iface_decls : env -> (FStar_Ident.lident * FStar_Parser_AST.decl Prims.list) Prims.list) = @@ -243,40 +238,28 @@ let (__proj__Mkenv__item__remaining_iface_decls : | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> remaining_iface_decls + ds_hooks; dep_graph;_} -> remaining_iface_decls let (__proj__Mkenv__item__syntax_only : env -> Prims.bool) = fun projectee -> match projectee with | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> syntax_only + ds_hooks; dep_graph;_} -> syntax_only let (__proj__Mkenv__item__ds_hooks : env -> dsenv_hooks) = fun projectee -> match projectee with | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> ds_hooks + ds_hooks; dep_graph;_} -> ds_hooks let (__proj__Mkenv__item__dep_graph : env -> FStar_Parser_Dep.deps) = fun projectee -> match projectee with | { curmodule; curmonad; modules; scope_mods; exported_ids; trans_exported_ids; includes; sigaccum; sigmap; iface; admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> dep_graph -let (__proj__Mkenv__item__opens_and_abbrevs_of : - env -> - (FStar_Syntax_Syntax.open_module_or_namespace, - FStar_Syntax_Syntax.module_abbrev) FStar_Pervasives.either Prims.list - FStar_Compiler_Util.smap) - = - fun projectee -> - match projectee with - | { curmodule; curmonad; modules; scope_mods; exported_ids; - trans_exported_ids; includes; sigaccum; sigmap; iface; - admitted_iface; expect_typ; remaining_iface_decls; syntax_only; - ds_hooks; dep_graph; opens_and_abbrevs_of;_} -> opens_and_abbrevs_of + ds_hooks; dep_graph;_} -> dep_graph let (__proj__Mkdsenv_hooks__item__ds_push_open_hook : dsenv_hooks -> env -> FStar_Syntax_Syntax.open_module_or_namespace -> unit) = @@ -353,8 +336,7 @@ let (set_iface : env -> Prims.bool -> env) = remaining_iface_decls = (env1.remaining_iface_decls); syntax_only = (env1.syntax_only); ds_hooks = (env1.ds_hooks); - dep_graph = (env1.dep_graph); - opens_and_abbrevs_of = (env1.opens_and_abbrevs_of) + dep_graph = (env1.dep_graph) } let (iface : env -> Prims.bool) = fun e -> e.iface let (set_admitted_iface : env -> Prims.bool -> env) = @@ -376,8 +358,7 @@ let (set_admitted_iface : env -> Prims.bool -> env) = remaining_iface_decls = (e.remaining_iface_decls); syntax_only = (e.syntax_only); ds_hooks = (e.ds_hooks); - dep_graph = (e.dep_graph); - opens_and_abbrevs_of = (e.opens_and_abbrevs_of) + dep_graph = (e.dep_graph) } let (admitted_iface : env -> Prims.bool) = fun e -> e.admitted_iface let (set_expect_typ : env -> Prims.bool -> env) = @@ -399,8 +380,7 @@ let (set_expect_typ : env -> Prims.bool -> env) = remaining_iface_decls = (e.remaining_iface_decls); syntax_only = (e.syntax_only); ds_hooks = (e.ds_hooks); - dep_graph = (e.dep_graph); - opens_and_abbrevs_of = (e.opens_and_abbrevs_of) + dep_graph = (e.dep_graph) } let (expect_typ : env -> Prims.bool) = fun e -> e.expect_typ let (all_exported_id_kinds : exported_id_kind Prims.list) = @@ -434,20 +414,6 @@ let (opens_and_abbrevs : | Open_module_or_namespace payload -> [FStar_Pervasives.Inl payload] | Module_abbrev (id, lid) -> [FStar_Pervasives.Inr (id, lid)] | uu___1 -> []) env1.scope_mods -let (opens_and_abbrevs_of : - env -> - FStar_Ident.lident -> - (FStar_Syntax_Syntax.open_module_or_namespace, - FStar_Syntax_Syntax.module_abbrev) FStar_Pervasives.either Prims.list) - = - fun env1 -> - fun lid -> - let uu___ = - let uu___1 = FStar_Ident.string_of_lid lid in - FStar_Compiler_Util.smap_try_find env1.opens_and_abbrevs_of uu___1 in - match uu___ with - | FStar_Pervasives_Native.None -> [] - | FStar_Pervasives_Native.Some l -> l let (open_modules : env -> (FStar_Ident.lident * FStar_Syntax_Syntax.modul) Prims.list) = fun e -> e.modules @@ -486,8 +452,7 @@ let (set_current_module : env -> FStar_Ident.lident -> env) = remaining_iface_decls = (e.remaining_iface_decls); syntax_only = (e.syntax_only); ds_hooks = (e.ds_hooks); - dep_graph = (e.dep_graph); - opens_and_abbrevs_of = (e.opens_and_abbrevs_of) + dep_graph = (e.dep_graph) } let (current_module : env -> FStar_Ident.lident) = fun env1 -> @@ -539,8 +504,7 @@ let (set_iface_decls : remaining_iface_decls = ((l, ds) :: rest); syntax_only = (env1.syntax_only); ds_hooks = (env1.ds_hooks); - dep_graph = (env1.dep_graph); - opens_and_abbrevs_of = (env1.opens_and_abbrevs_of) + dep_graph = (env1.dep_graph) } let (qual : FStar_Ident.lident -> FStar_Ident.ident -> FStar_Ident.lident) = FStar_Ident.qual_id @@ -573,8 +537,7 @@ let (set_syntax_only : env -> Prims.bool -> env) = remaining_iface_decls = (env1.remaining_iface_decls); syntax_only = b; ds_hooks = (env1.ds_hooks); - dep_graph = (env1.dep_graph); - opens_and_abbrevs_of = (env1.opens_and_abbrevs_of) + dep_graph = (env1.dep_graph) } let (ds_hooks : env -> dsenv_hooks) = fun env1 -> env1.ds_hooks let (set_ds_hooks : env -> dsenv_hooks -> env) = @@ -596,8 +559,7 @@ let (set_ds_hooks : env -> dsenv_hooks -> env) = remaining_iface_decls = (env1.remaining_iface_decls); syntax_only = (env1.syntax_only); ds_hooks = hooks; - dep_graph = (env1.dep_graph); - opens_and_abbrevs_of = (env1.opens_and_abbrevs_of) + dep_graph = (env1.dep_graph) } let new_sigmap : 'uuuuu . unit -> 'uuuuu FStar_Compiler_Util.smap = fun uu___ -> FStar_Compiler_Util.smap_create (Prims.of_int (100)) @@ -607,7 +569,6 @@ let (empty_env : FStar_Parser_Dep.deps -> env) = let uu___1 = new_sigmap () in let uu___2 = new_sigmap () in let uu___3 = new_sigmap () in - let uu___4 = new_sigmap () in { curmodule = FStar_Pervasives_Native.None; curmonad = FStar_Pervasives_Native.None; @@ -624,8 +585,7 @@ let (empty_env : FStar_Parser_Dep.deps -> env) = remaining_iface_decls = []; syntax_only = false; ds_hooks = default_ds_hooks; - dep_graph = deps; - opens_and_abbrevs_of = uu___4 + dep_graph = deps } let (dep_graph : env -> FStar_Parser_Dep.deps) = fun env1 -> env1.dep_graph let (set_dep_graph : env -> FStar_Parser_Dep.deps -> env) = @@ -647,8 +607,7 @@ let (set_dep_graph : env -> FStar_Parser_Dep.deps -> env) = remaining_iface_decls = (env1.remaining_iface_decls); syntax_only = (env1.syntax_only); ds_hooks = (env1.ds_hooks); - dep_graph = ds; - opens_and_abbrevs_of = (env1.opens_and_abbrevs_of) + dep_graph = ds } let (sigmap : env -> (FStar_Syntax_Syntax.sigelt * Prims.bool) FStar_Compiler_Util.smap) @@ -1865,8 +1824,7 @@ let (try_lookup_lid_with_attributes_no_resolve : remaining_iface_decls = (env1.remaining_iface_decls); syntax_only = (env1.syntax_only); ds_hooks = (env1.ds_hooks); - dep_graph = (env1.dep_graph); - opens_and_abbrevs_of = (env1.opens_and_abbrevs_of) + dep_graph = (env1.dep_graph) } in try_lookup_lid_with_attributes env' l let (try_lookup_lid_no_resolve : @@ -2400,8 +2358,7 @@ let (unique : remaining_iface_decls = (env1.remaining_iface_decls); syntax_only = (env1.syntax_only); ds_hooks = (env1.ds_hooks); - dep_graph = (env1.dep_graph); - opens_and_abbrevs_of = (env1.opens_and_abbrevs_of) + dep_graph = (env1.dep_graph) } in let uu___ = try_lookup_lid' any_val exclude_interface this_env lid in match uu___ with @@ -2426,8 +2383,7 @@ let (push_scope_mod : env -> scope_mod -> env) = remaining_iface_decls = (env1.remaining_iface_decls); syntax_only = (env1.syntax_only); ds_hooks = (env1.ds_hooks); - dep_graph = (env1.dep_graph); - opens_and_abbrevs_of = (env1.opens_and_abbrevs_of) + dep_graph = (env1.dep_graph) } let (push_bv' : env -> FStar_Ident.ident -> (env * FStar_Syntax_Syntax.bv * used_marker)) = @@ -2551,8 +2507,7 @@ let (push_sigelt' : Prims.bool -> env -> FStar_Syntax_Syntax.sigelt -> env) = remaining_iface_decls = (env1.remaining_iface_decls); syntax_only = (env1.syntax_only); ds_hooks = (env1.ds_hooks); - dep_graph = (env1.dep_graph); - opens_and_abbrevs_of = (env1.opens_and_abbrevs_of) + dep_graph = (env1.dep_graph) })) in let env3 = let uu___ = FStar_Compiler_Effect.op_Bang globals in @@ -2572,8 +2527,7 @@ let (push_sigelt' : Prims.bool -> env -> FStar_Syntax_Syntax.sigelt -> env) = remaining_iface_decls = (env2.remaining_iface_decls); syntax_only = (env2.syntax_only); ds_hooks = (env2.ds_hooks); - dep_graph = (env2.dep_graph); - opens_and_abbrevs_of = (env2.opens_and_abbrevs_of) + dep_graph = (env2.dep_graph) } in let uu___ = match s.FStar_Syntax_Syntax.sigel with @@ -2665,8 +2619,7 @@ let (push_sigelt' : Prims.bool -> env -> FStar_Syntax_Syntax.sigelt -> env) = remaining_iface_decls = (env4.remaining_iface_decls); syntax_only = (env4.syntax_only); ds_hooks = (env4.ds_hooks); - dep_graph = (env4.dep_graph); - opens_and_abbrevs_of = (env4.opens_and_abbrevs_of) + dep_graph = (env4.dep_graph) } in env5)) let (push_sigelt : env -> FStar_Syntax_Syntax.sigelt -> env) = @@ -3617,29 +3570,25 @@ let (finish : env -> FStar_Syntax_Syntax.modul -> env) = (filter_record_cache (); (match () with | () -> - let opens_and_abbrevs1 = opens_and_abbrevs env1 in - (FStar_Compiler_Util.smap_add env1.opens_and_abbrevs_of - curmod opens_and_abbrevs1; - { - curmodule = FStar_Pervasives_Native.None; - curmonad = (env1.curmonad); - modules = (((modul.FStar_Syntax_Syntax.name), modul) :: - (env1.modules)); - scope_mods = []; - exported_ids = (env1.exported_ids); - trans_exported_ids = (env1.trans_exported_ids); - includes = (env1.includes); - sigaccum = []; - sigmap = (env1.sigmap); - iface = (env1.iface); - admitted_iface = (env1.admitted_iface); - expect_typ = (env1.expect_typ); - remaining_iface_decls = (env1.remaining_iface_decls); - syntax_only = (env1.syntax_only); - ds_hooks = (env1.ds_hooks); - dep_graph = (env1.dep_graph); - opens_and_abbrevs_of = (env1.opens_and_abbrevs_of) - }))))) + { + curmodule = FStar_Pervasives_Native.None; + curmonad = (env1.curmonad); + modules = (((modul.FStar_Syntax_Syntax.name), modul) :: + (env1.modules)); + scope_mods = []; + exported_ids = (env1.exported_ids); + trans_exported_ids = (env1.trans_exported_ids); + includes = (env1.includes); + sigaccum = []; + sigmap = (env1.sigmap); + iface = (env1.iface); + admitted_iface = (env1.admitted_iface); + expect_typ = (env1.expect_typ); + remaining_iface_decls = (env1.remaining_iface_decls); + syntax_only = (env1.syntax_only); + ds_hooks = (env1.ds_hooks); + dep_graph = (env1.dep_graph) + })))) let (stack : env Prims.list FStar_Compiler_Effect.ref) = FStar_Compiler_Util.mk_ref [] let (push : env -> env) = @@ -3671,8 +3620,7 @@ let (push : env -> env) = remaining_iface_decls = (env1.remaining_iface_decls); syntax_only = (env1.syntax_only); ds_hooks = (env1.ds_hooks); - dep_graph = (env1.dep_graph); - opens_and_abbrevs_of = (env1.opens_and_abbrevs_of) + dep_graph = (env1.dep_graph) })) let (pop : unit -> env) = fun uu___ -> @@ -3844,30 +3792,6 @@ let (inclusion_info : env -> FStar_Ident.lident -> module_inclusion_info) = mii_trans_exported_ids = uu___1; mii_includes = uu___2 } -let (includes_of : module_inclusion_info -> FStar_Ident.lident Prims.list) = - fun m -> - match m.mii_includes with - | FStar_Pervasives_Native.None -> [] - | FStar_Pervasives_Native.Some l -> - FStar_Compiler_List.map FStar_Pervasives_Native.fst l -let (transitive_includes_of : - env -> FStar_Ident.lident -> FStar_Ident.lident Prims.list) = - fun env1 -> - fun modul -> - let rec transitive_includes_of1 acc modul1 = - let mii = inclusion_info env1 modul1 in - let includes = includes_of mii in - FStar_Compiler_List.fold_left - (fun acc1 -> - fun i -> - let uu___ = - FStar_Compiler_Util.for_some (FStar_Ident.lid_equals i) acc1 in - if uu___ - then acc1 - else - (let uu___2 = transitive_includes_of1 acc1 i in i :: uu___2)) - acc includes in - transitive_includes_of1 [] modul let (prepare_module_or_interface : Prims.bool -> Prims.bool -> @@ -3959,9 +3883,7 @@ let (prepare_module_or_interface : (env2.remaining_iface_decls); syntax_only = (env2.syntax_only); ds_hooks = (env2.ds_hooks); - dep_graph = (env2.dep_graph); - opens_and_abbrevs_of = - (env2.opens_and_abbrevs_of) + dep_graph = (env2.dep_graph) } in (FStar_Compiler_List.iter (fun op -> @@ -4032,8 +3954,7 @@ let (enter_monad_scope : env -> FStar_Ident.ident -> env) = remaining_iface_decls = (env1.remaining_iface_decls); syntax_only = (env1.syntax_only); ds_hooks = (env1.ds_hooks); - dep_graph = (env1.dep_graph); - opens_and_abbrevs_of = (env1.opens_and_abbrevs_of) + dep_graph = (env1.dep_graph) } let fail_or : 'a . diff --git a/src/syntax/FStar.Syntax.DsEnv.fst b/src/syntax/FStar.Syntax.DsEnv.fst index 0316d004a5e..a484c28b785 100644 --- a/src/syntax/FStar.Syntax.DsEnv.fst +++ b/src/syntax/FStar.Syntax.DsEnv.fst @@ -85,8 +85,7 @@ type env = { remaining_iface_decls:list (lident&list Parser.AST.decl); (* A map from interface names to their stil-to-be-processed top-level decls *) syntax_only: bool; (* Whether next push should skip type-checking *) ds_hooks: dsenv_hooks; (* hooks that the interactive more relies onto for symbol tracking *) - dep_graph: FStar.Parser.Dep.deps; - opens_and_abbrevs_of: BU.smap (list (either open_module_or_namespace module_abbrev)); + dep_graph: FStar.Parser.Dep.deps } and dsenv_hooks = { ds_push_open_hook : env -> open_module_or_namespace -> unit; @@ -122,10 +121,7 @@ let opens_and_abbrevs env : list (either open_module_or_namespace module_abbrev) | Module_abbrev (id, lid) -> [Inr (id, lid)] | _ -> []) env.scope_mods -let opens_and_abbrevs_of env lid = - match BU.smap_try_find env.opens_and_abbrevs_of (Ident.string_of_lid lid) with - | None -> [] - | Some l -> l + let open_modules e = e.modules let open_modules_and_namespaces env = List.filter_map (function @@ -177,8 +173,7 @@ let empty_env deps = {curmodule=None; remaining_iface_decls=[]; syntax_only=false; ds_hooks=default_ds_hooks; - dep_graph=deps; - opens_and_abbrevs_of=new_sigmap()} + dep_graph=deps} let dep_graph env = env.dep_graph let set_dep_graph env ds = {env with dep_graph=ds} let sigmap env = env.sigmap @@ -1323,8 +1318,6 @@ let finish env modul = in (* remove abstract/private records *) let () = filter_record_cache () in - let opens_and_abbrevs = opens_and_abbrevs env in - BU.smap_add env.opens_and_abbrevs_of curmod opens_and_abbrevs; {env with curmodule=None; modules=(modul.name, modul)::env.modules; @@ -1428,23 +1421,6 @@ let inclusion_info env (l:lident) = mii_trans_exported_ids = as_ids_opt env.trans_exported_ids; mii_includes = BU.map_opt (BU.smap_try_find env.includes mname) (fun r -> !r) } -let includes_of (m:module_inclusion_info) = - match m.mii_includes with - | None -> [] - | Some l -> List.map fst l -let transitive_includes_of (env:env) (modul:lident) -: list lident -= let rec transitive_includes_of (acc: list lident) (modul:lident) - : list lident - = let mii = inclusion_info env modul in - let includes = includes_of mii in - List.fold_left - (fun acc i -> - if BU.for_some (Ident.lid_equals i) acc - then acc - else i::transitive_includes_of acc i) - acc includes - in transitive_includes_of [] modul let prepare_module_or_interface intf admitted env mname (mii:module_inclusion_info) = (* AR: open the pervasives namespace *) let prep env = diff --git a/src/syntax/FStar.Syntax.DsEnv.fsti b/src/syntax/FStar.Syntax.DsEnv.fsti index abec790be84..08d7cc57a7f 100644 --- a/src/syntax/FStar.Syntax.DsEnv.fsti +++ b/src/syntax/FStar.Syntax.DsEnv.fsti @@ -63,7 +63,6 @@ val fail_or: env -> (lident -> option 'a) -> lident -> 'a val fail_or2: (ident -> option 'a) -> ident -> 'a val opens_and_abbrevs :env -> list (either open_module_or_namespace module_abbrev) -val opens_and_abbrevs_of : env -> lident -> list (either open_module_or_namespace module_abbrev) val dep_graph: env -> FStar.Parser.Dep.deps val set_dep_graph: env -> FStar.Parser.Dep.deps -> env val ds_hooks : env -> dsenv_hooks @@ -138,7 +137,6 @@ val transitive_exported_ids: env -> lident -> list string val module_inclusion_info : Type0 val default_mii : module_inclusion_info val inclusion_info: env -> lident -> module_inclusion_info -val transitive_includes_of (_:env) (modul:lident) : list lident val prepare_module_or_interface: bool -> bool -> env -> lident -> module_inclusion_info -> env & bool //pop the context when done desugaring (* private *) val try_lookup_lid': bool -> bool -> env -> lident -> option (term & list attribute) diff --git a/src/syntax/FStar.Syntax.VisitM.fst b/src/syntax/FStar.Syntax.VisitM.fst index 412feaf731c..ab125b3234d 100644 --- a/src/syntax/FStar.Syntax.VisitM.fst +++ b/src/syntax/FStar.Syntax.VisitM.fst @@ -537,5 +537,4 @@ in let lids, _ = Writer.run_writer m in BU.print1 "Lids = %s\n" (show lids); -*) -////////////////////////////////////////////////////////////////// \ No newline at end of file +*) \ No newline at end of file diff --git a/src/typechecker/FStar.TypeChecker.ContextPruning.fst b/src/typechecker/FStar.TypeChecker.ContextPruning.fst deleted file mode 100644 index caaeeba90d9..00000000000 --- a/src/typechecker/FStar.TypeChecker.ContextPruning.fst +++ /dev/null @@ -1,223 +0,0 @@ -module FStar.TypeChecker.ContextPruning -open FStar.Compiler -open FStar.Compiler.Effect -open FStar.Ident -open FStar.Syntax.Syntax -open FStar.TypeChecker.Env -open FStar.Class.Monad -open FStar.Class.Show -open FStar.List.Tot -module BU = FStar.Compiler.Util -module SS = FStar.Syntax.Subst -open FStar.Class.Setlike - -let lid_set = FStar.Compiler.RBSet.rbset lident - -type ctxt = { - env: env; - reached: lid_set; - pending_lemmas: pending_lemma_patterns; -} - - -let st a = ctxt -> (a & ctxt) -let get : st ctxt = fun s -> (s, s) -let put (c:ctxt) : st unit = fun _ -> ((), c) -instance st_monad: monad st = { - return= (fun (#a:Type) (x:a) -> (fun s -> (x, s)) <: st a); - ( let! ) = (fun (#a #b:Type) (m:st a) (f:a -> st b) (s:ctxt) -> - let (x, s) = m s in - f x s) -} - -let remove_trigger (lid:lident) -: st unit -= let! ctxt = get in - put {ctxt with pending_lemmas=remove_pending_lemma lid ctxt.pending_lemmas} - -let find_lemmas_waiting_on_trigger (lid:lident) -: st (list lident) -= let! ctxt = get in - let lems = Env.find_lemmas_waiting_on_trigger lid ctxt.pending_lemmas in - // BU.print2 "Lemmas waiting on trigger %s = %s\n" (show lid) (show lems); - return lems - -let add_lident (x:lident) -: st unit -= let! ctxt = get in - put {ctxt with reached=add x ctxt.reached} - -let remove_trigger_for_lemma (pat:lident) (lem:lident) -: st bool -= let! ctxt = get in - // BU.print2 "Removing trigger %s for %s\n" (show pat) (show lem); - let pp, eligible = Env.remove_trigger_for_lemma pat lem ctxt.pending_lemmas in - put {ctxt with pending_lemmas=pp} ;! - // let! _ = - // if eligible - // then add_lident lem - // else return () in - return eligible - -let ctx_contains (x:lident) -: st bool -= let! ctxt = get in - return (mem x ctxt.reached) - -let reachable_of_inductive env (ty:lident) -= let aux (a_lids, a_tys) ty = - let _,dcs = Env.datacons_of_typ env ty in - let tys = - List.collect - (fun dc -> - match Env.try_lookup_lid env dc with - | None -> [] - | Some ((_, t), _) -> [t]) - dcs - in - let tys = - match Env.try_lookup_lid env ty with - | None -> tys - | Some ((_, t), _) -> t::tys - in - dcs@a_lids, tys@a_tys - in - let aux mutuals = List.fold_left aux ([], []) mutuals in - match Env.lookup_qname env ty with - | Some (Inr (se, _), _) -> ( - match se.sigel with - | Sig_inductive_typ { mutuals } -> aux mutuals - | _ -> [], [] - ) - | _ -> [], [] - -let lookup_lident_in_env env (x:lident) -: list lident //identifiers reachable from x - & list term //terms that need to be scanned= -= match Env.lookup_qname env x with - | None -> [], [] - | Some (Inl (_, t), _) -> [], [t] - | Some (Inr (se, _), _) -> ( - match se.sigel with - | Sig_inductive_typ { lid } -> reachable_of_inductive env lid - | Sig_datacon { ty_lid } -> reachable_of_inductive env ty_lid - | Sig_declare_typ { t } -> [], [t] - | Sig_let { lbs; lids=mutuals } -> - mutuals, - snd lbs |> List.collect (fun lb -> [lb.lbtyp; lb.lbdef]) - | Sig_assume { phi } -> [], [phi] - | _ -> [], [] - ) - -let lookup_definition_and_type (x:lident) -: st (list lident & list term) -= let open FStar.TypeChecker.Env in - let! ctxt = get in - let res = lookup_lident_in_env ctxt.env x in - return res - // let def = - // match lookup_definition [Env.Unfold delta_constant] ctxt.env x with - // | None -> [] - // | Some (_, t) -> [t] - // in - // return <| - // (match try_lookup_lid ctxt.env x with - // | None -> def - // | Some ((_, t),_) -> t::def) - - -let lookup_type (x:lident) -: st (option term) -= let! ctxt = get in - match Env.try_lookup_lid ctxt.env x with - | None -> - return None - | Some ((_, t), _) -> return (Some t) - -let rec context_of_term (t:term) -: st (list lident) -= let fvs = FStar.Syntax.Free.fvars t in - foldM_left - (fun acc fv -> - if! ctx_contains fv - then return acc - else ( - add_lident fv ;! - let! lids, terms = lookup_definition_and_type fv in - iterM (fun lid -> add_lident lid) lids ;! - foldM_left - (fun acc t -> - let! fvs = context_of_term t in - return (fvs @ acc)) - (fv::lids@acc) terms)) - [] - (elems fvs) - -let trigger_pending_lemmas (lids:list lident) -: st (either (list lident) bool) //either some lemmas were triggered; or maybe nothing changed -= let join_acc acc next = - match acc, next with - | Inl l, Inl m -> Inl (l @ m) - | Inl l, Inr _ -> Inl l - | Inr _, Inl m -> Inl m - | Inr l, Inr m -> Inr (l || m) - in - foldM_left - (fun acc lid -> - match! find_lemmas_waiting_on_trigger lid with - | [] -> return acc - | lemmas -> - remove_trigger lid ;! - let! eligible_lemmas = - foldM_left - (fun acc lem -> - if! remove_trigger_for_lemma lid lem - then return (lem::acc) - else return acc) - [] - lemmas - in - match eligible_lemmas with - | [] -> return (join_acc acc <| Inr true) //something changed - | _ -> return (join_acc acc <| Inl eligible_lemmas)) - (Inr false) - lids -open FStar.List.Tot -let rec scan (ts:list term) -: st unit -= let! new_fvs = - foldM_left - (fun acc t -> - let! new_fvs = context_of_term t in - return (new_fvs @ acc)) - [] ts - in - // BU.print1 "Scanned terms got %s\n" (show new_fvs); - match! trigger_pending_lemmas new_fvs with - | Inl triggered -> - let! lemma_types = - foldM_left - (fun acc lem -> - if! ctx_contains lem - then ( - return acc - ) - else ( - add_lident lem ;! - match! lookup_type lem with - | None -> return acc - | Some t -> - return (t::acc) - )) - [] - triggered - in - scan lemma_types - | Inr _ -> return () - -let context_of (env:env) (ts:list term) -: list lident -= let init = { env; pending_lemmas=env.pending_lemmas; reached=empty() } in - let ambients = List.map (fun x -> lid_as_fv x None |> fv_to_tm) (Env.ambients env.pending_lemmas) in - let _, ctxt = scan (ts@ambients) init in - elems ctxt.reached \ No newline at end of file diff --git a/src/typechecker/FStar.TypeChecker.ContextPruning.fsti b/src/typechecker/FStar.TypeChecker.ContextPruning.fsti deleted file mode 100644 index ed515c01084..00000000000 --- a/src/typechecker/FStar.TypeChecker.ContextPruning.fsti +++ /dev/null @@ -1,5 +0,0 @@ -module FStar.TypeChecker.ContextPruning -open FStar.Syntax.Syntax -open FStar.TypeChecker.Env -open FStar.Ident -val context_of (env:env) (t:list term) : list lident \ No newline at end of file