Merge pull request #3579 from FStarLang/nik_gamma_sig_no_mtime

Fix some quadratic name lookup behavior

src/smtencoding/FStarC.SMTEncoding.Encode.fst

@@ -112,12 +112,12 @@ let prims =
               let app = mk_Apply app [var] in
               let vars = vars @ [var] in
               let axiom_name = axiom_name ^ "." ^ (string_of_int (vars |> List.length)) in
-              axioms @ [Util.mkAssume (mkForall rng ([[app]], vars, mk_IsTotFun app), None, axiom_name)],
+              Util.mkAssume (mkForall rng ([[app]], vars, mk_IsTotFun app), None, axiom_name) :: axioms,
               app,
               vars
             ) ([tot_fun_axiom_for_x], xtok, []) all_vars_but_one
           in
-          axioms
+          List.rev axioms
         in
 
         let rel_body =
@@ -598,9 +598,12 @@ let encode_top_level_val uninterpreted env us fv t quals =
     else decls, env
 
 let encode_top_level_vals env bindings quals =
+  let decls, env =
     bindings |> List.fold_left (fun (decls, env) lb ->
         let decls', env = encode_top_level_val false env lb.lbunivs (BU.right lb.lbname) lb.lbtyp quals in
-        decls@decls', env) ([], env)
+        List.rev_append decls' decls, env) ([], env)
+  in
+  List.rev decls, env
 
 exception Let_rec_unencodeable
 
@@ -1954,9 +1957,12 @@ let encode_modul tcenv modul =
     then BU.print2 "+++++++++++Encoding externals for %s ... %s declarations\n" name (List.length modul.declarations |> string_of_int);
     let env = get_env modul.name tcenv |> reset_current_module_fvbs in
     let encode_signature (env:env_t) (ses:sigelts) =
+      let g', env =
         ses |> List.fold_left (fun (g, env) se ->
           let g', env = encode_top_level_facts env se in
-          g@g', env) ([], env)
+          List.rev_append g' g, env) ([], env)
+      in
+      List.rev g', env
     in
     let decls, env = encode_signature ({env with warn=false}) modul.declarations in
     give_decls_to_z3_and_set_env env name decls;

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=[];