diff --git a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Encode.ml b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Encode.ml index 92a739589bc..03b60e497b9 100644 --- a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Encode.ml +++ b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Encode.ml @@ -201,22 +201,20 @@ let (prims : prims_t) = let uu___8 = let uu___9 = let uu___10 = - let uu___11 = - FStarC_SMTEncoding_Term.mk_IsTotFun - app1 in - ([[app1]], vars2, uu___11) in - FStarC_SMTEncoding_Term.mkForall - rng uu___10 in - (uu___9, - FStar_Pervasives_Native.None, - axiom_name1) in - FStarC_SMTEncoding_Util.mkAssume - uu___8 in - [uu___7] in - FStarC_Compiler_List.op_At axioms uu___6 in + FStarC_SMTEncoding_Term.mk_IsTotFun + app1 in + ([[app1]], vars2, uu___10) in + FStarC_SMTEncoding_Term.mkForall rng + uu___9 in + (uu___8, FStar_Pervasives_Native.None, + axiom_name1) in + FStarC_SMTEncoding_Util.mkAssume uu___7 in + uu___6 :: axioms in (uu___5, app1, vars2)) ([tot_fun_axiom_for_x], xtok1, []) all_vars_but_one in - match uu___3 with | (axioms, uu___4, uu___5) -> axioms in + match uu___3 with + | (axioms, uu___4, uu___5) -> + FStarC_Compiler_List.rev axioms in let rel_body = let rel_body1 = rel_type_f rel (xapp, body) in match precondition with @@ -2363,22 +2361,25 @@ let (encode_top_level_vals : fun env -> fun bindings -> fun quals -> - FStarC_Compiler_List.fold_left - (fun uu___ -> - fun lb -> - match uu___ with - | (decls, env1) -> - let uu___1 = + let uu___ = + FStarC_Compiler_List.fold_left + (fun uu___1 -> + fun lb -> + match uu___1 with + | (decls, env1) -> let uu___2 = - FStarC_Compiler_Util.right - lb.FStarC_Syntax_Syntax.lbname in - encode_top_level_val false env1 - lb.FStarC_Syntax_Syntax.lbunivs uu___2 - lb.FStarC_Syntax_Syntax.lbtyp quals in - (match uu___1 with - | (decls', env2) -> - ((FStarC_Compiler_List.op_At decls decls'), env2))) - ([], env) bindings + let uu___3 = + FStarC_Compiler_Util.right + lb.FStarC_Syntax_Syntax.lbname in + encode_top_level_val false env1 + lb.FStarC_Syntax_Syntax.lbunivs uu___3 + lb.FStarC_Syntax_Syntax.lbtyp quals in + (match uu___2 with + | (decls', env2) -> + ((FStarC_Compiler_List.rev_append decls' decls), + env2))) ([], env) bindings in + match uu___ with + | (decls, env1) -> ((FStarC_Compiler_List.rev decls), env1) exception Let_rec_unencodeable let (uu___is_Let_rec_unencodeable : Prims.exn -> Prims.bool) = fun projectee -> @@ -7675,16 +7676,19 @@ let (encode_modul : let uu___5 = get_env modul.FStarC_Syntax_Syntax.name tcenv1 in FStarC_SMTEncoding_Env.reset_current_module_fvbs uu___5 in let encode_signature env1 ses = - FStarC_Compiler_List.fold_left - (fun uu___5 -> - fun se -> - match uu___5 with - | (g, env2) -> - let uu___6 = encode_top_level_facts env2 se in - (match uu___6 with - | (g', env3) -> - ((FStarC_Compiler_List.op_At g g'), env3))) - ([], env1) ses in + let uu___5 = + FStarC_Compiler_List.fold_left + (fun uu___6 -> + fun se -> + match uu___6 with + | (g, env2) -> + let uu___7 = encode_top_level_facts env2 se in + (match uu___7 with + | (g', env3) -> + ((FStarC_Compiler_List.rev_append g' g), + env3))) ([], env1) ses in + match uu___5 with + | (g', env2) -> ((FStarC_Compiler_List.rev g'), env2) in let uu___5 = encode_signature { 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/smtencoding/FStarC.SMTEncoding.Encode.fst b/src/smtencoding/FStarC.SMTEncoding.Encode.fst index 7d813f53411..a3ebb108bcc 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Encode.fst +++ b/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; 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=[];