diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml index dbfe7f06e7b..5fa3195d52e 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml @@ -3761,1275 +3761,567 @@ let (encode_top_level_let : (Prims.strcat "let rec unencodeable: Skipping: " msg) in let uu___2 = FStar_SMTEncoding_Term.mk_decls_trivial [decl] in (uu___2, env)) -let rec (encode_sigelt : - FStar_SMTEncoding_Env.env_t -> - FStar_Syntax_Syntax.sigelt -> - (FStar_SMTEncoding_Term.decls_t * FStar_SMTEncoding_Env.env_t)) - = +let (is_sig_inductive_injective_on_params : + FStar_SMTEncoding_Env.env_t -> FStar_Syntax_Syntax.sigelt -> Prims.bool) = fun env -> fun se -> - let nm = FStar_Syntax_Print.sigelt_to_string_short se in - let uu___ = - let uu___1 = - let uu___2 = FStar_Syntax_Print.sigelt_to_string_short se in - FStar_Compiler_Util.format1 - "While encoding top-level declaration `%s`" uu___2 in - FStar_Errors.with_ctx uu___1 (fun uu___2 -> encode_sigelt' env se) in + let uu___ = se.FStar_Syntax_Syntax.sigel in match uu___ with - | (g, env1) -> - let g1 = - match g with - | [] -> - ((let uu___2 = - FStar_TypeChecker_Env.debug - env1.FStar_SMTEncoding_Env.tcenv - (FStar_Options.Other "SMTEncoding") in - if uu___2 - then - FStar_Compiler_Util.print1 "Skipped encoding of %s\n" nm - else ()); - (let uu___2 = - let uu___3 = - let uu___4 = - FStar_Compiler_Util.format1 "" nm in - FStar_SMTEncoding_Term.Caption uu___4 in - [uu___3] in - FStar_SMTEncoding_Term.mk_decls_trivial uu___2)) - | uu___1 -> - let uu___2 = - let uu___3 = - let uu___4 = - let uu___5 = - FStar_Compiler_Util.format1 "" nm in - FStar_SMTEncoding_Term.Caption uu___5 in - [uu___4] in - FStar_SMTEncoding_Term.mk_decls_trivial uu___3 in - let uu___3 = - let uu___4 = - let uu___5 = - let uu___6 = - let uu___7 = - FStar_Compiler_Util.format1 "" nm in - FStar_SMTEncoding_Term.Caption uu___7 in - [uu___6] in - FStar_SMTEncoding_Term.mk_decls_trivial uu___5 in - FStar_Compiler_List.op_At g uu___4 in - FStar_Compiler_List.op_At uu___2 uu___3 in - (g1, env1) -and (encode_sigelt' : - FStar_SMTEncoding_Env.env_t -> - FStar_Syntax_Syntax.sigelt -> - (FStar_SMTEncoding_Term.decls_t * FStar_SMTEncoding_Env.env_t)) + | FStar_Syntax_Syntax.Sig_inductive_typ + { FStar_Syntax_Syntax.lid = t; + FStar_Syntax_Syntax.us = universe_names; + FStar_Syntax_Syntax.params = tps; + FStar_Syntax_Syntax.num_uniform_params = uu___1; + FStar_Syntax_Syntax.t = k; FStar_Syntax_Syntax.mutuals = uu___2; + FStar_Syntax_Syntax.ds = uu___3;_} + -> + let t_lid = t in + let tcenv = env.FStar_SMTEncoding_Env.tcenv in + let uu___4 = FStar_Syntax_Subst.univ_var_opening universe_names in + (match uu___4 with + | (usubst, uvs) -> + let uu___5 = + let uu___6 = FStar_TypeChecker_Env.push_univ_vars tcenv uvs in + let uu___7 = FStar_Syntax_Subst.subst_binders usubst tps in + let uu___8 = + let uu___9 = + FStar_Syntax_Subst.shift_subst + (FStar_Compiler_List.length tps) usubst in + FStar_Syntax_Subst.subst uu___9 k in + (uu___6, uu___7, uu___8) in + (match uu___5 with + | (tcenv1, tps1, k1) -> + let uu___6 = FStar_Syntax_Subst.open_term tps1 k1 in + (match uu___6 with + | (tps2, k2) -> + let uu___7 = FStar_Syntax_Util.arrow_formals k2 in + (match uu___7 with + | (uu___8, k3) -> + let uu___9 = + FStar_TypeChecker_TcTerm.tc_binders tcenv1 + tps2 in + (match uu___9 with + | (tps3, env_tps, uu___10, us) -> + let u_k = + let uu___11 = + let uu___12 = + FStar_Syntax_Syntax.fvar t + FStar_Pervasives_Native.None in + let uu___13 = + let uu___14 = + FStar_Syntax_Util.args_of_binders + tps3 in + FStar_Pervasives_Native.snd uu___14 in + let uu___14 = + FStar_Ident.range_of_lid t in + FStar_Syntax_Syntax.mk_Tm_app uu___12 + uu___13 uu___14 in + FStar_TypeChecker_TcTerm.level_of_type + env_tps uu___11 k3 in + let rec universe_leq u v = + match (u, v) with + | (FStar_Syntax_Syntax.U_zero, uu___11) + -> true + | (FStar_Syntax_Syntax.U_succ u0, + FStar_Syntax_Syntax.U_succ v0) -> + universe_leq u0 v0 + | (FStar_Syntax_Syntax.U_name u0, + FStar_Syntax_Syntax.U_name v0) -> + FStar_Ident.ident_equals u0 v0 + | (FStar_Syntax_Syntax.U_name uu___11, + FStar_Syntax_Syntax.U_succ v0) -> + universe_leq u v0 + | (FStar_Syntax_Syntax.U_max us1, + uu___11) -> + FStar_Compiler_Util.for_all + (fun u1 -> universe_leq u1 v) us1 + | (uu___11, FStar_Syntax_Syntax.U_max + vs) -> + FStar_Compiler_Util.for_some + (universe_leq u) vs + | (FStar_Syntax_Syntax.U_unknown, + uu___11) -> + let uu___12 = + let uu___13 = + FStar_Ident.string_of_lid t in + let uu___14 = + FStar_Syntax_Print.univ_to_string + u in + let uu___15 = + FStar_Syntax_Print.univ_to_string + v in + FStar_Compiler_Util.format3 + "Impossible: Unresolved or unknown universe in inductive type %s (%s, %s)" + uu___13 uu___14 uu___15 in + FStar_Compiler_Effect.failwith + uu___12 + | (uu___11, + FStar_Syntax_Syntax.U_unknown) -> + let uu___12 = + let uu___13 = + FStar_Ident.string_of_lid t in + let uu___14 = + FStar_Syntax_Print.univ_to_string + u in + let uu___15 = + FStar_Syntax_Print.univ_to_string + v in + FStar_Compiler_Util.format3 + "Impossible: Unresolved or unknown universe in inductive type %s (%s, %s)" + uu___13 uu___14 uu___15 in + FStar_Compiler_Effect.failwith + uu___12 + | (FStar_Syntax_Syntax.U_unif uu___11, + uu___12) -> + let uu___13 = + let uu___14 = + FStar_Ident.string_of_lid t in + let uu___15 = + FStar_Syntax_Print.univ_to_string + u in + let uu___16 = + FStar_Syntax_Print.univ_to_string + v in + FStar_Compiler_Util.format3 + "Impossible: Unresolved or unknown universe in inductive type %s (%s, %s)" + uu___14 uu___15 uu___16 in + FStar_Compiler_Effect.failwith + uu___13 + | (uu___11, FStar_Syntax_Syntax.U_unif + uu___12) -> + let uu___13 = + let uu___14 = + FStar_Ident.string_of_lid t in + let uu___15 = + FStar_Syntax_Print.univ_to_string + u in + let uu___16 = + FStar_Syntax_Print.univ_to_string + v in + FStar_Compiler_Util.format3 + "Impossible: Unresolved or unknown universe in inductive type %s (%s, %s)" + uu___14 uu___15 uu___16 in + FStar_Compiler_Effect.failwith + uu___13 + | uu___11 -> false in + let u_leq_u_k u = + let u1 = + FStar_TypeChecker_Normalize.normalize_universe + env_tps u in + universe_leq u1 u_k in + let tp_ok tp u_tp = + let t_tp = + (tp.FStar_Syntax_Syntax.binder_bv).FStar_Syntax_Syntax.sort in + let uu___11 = u_leq_u_k u_tp in + if uu___11 + then true + else + (let t_tp1 = + FStar_TypeChecker_Normalize.normalize + [FStar_TypeChecker_Env.Unrefine; + FStar_TypeChecker_Env.Unascribe; + FStar_TypeChecker_Env.Unmeta; + FStar_TypeChecker_Env.Primops; + FStar_TypeChecker_Env.HNF; + FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.Beta] + env_tps t_tp in + let uu___13 = + FStar_Syntax_Util.arrow_formals + t_tp1 in + match uu___13 with + | (formals, t1) -> + let uu___14 = + FStar_TypeChecker_TcTerm.tc_binders + env_tps formals in + (match uu___14 with + | (uu___15, uu___16, uu___17, + u_formals) -> + let inj = + FStar_Compiler_Util.for_all + (fun u_formal -> + u_leq_u_k u_formal) + u_formals in + if inj + then + let uu___18 = + let uu___19 = + FStar_Syntax_Subst.compress + t1 in + uu___19.FStar_Syntax_Syntax.n in + (match uu___18 with + | FStar_Syntax_Syntax.Tm_type + u -> u_leq_u_k u + | uu___19 -> false) + else false)) in + let is_injective_on_params = + FStar_Compiler_List.forall2 tp_ok tps3 + us in + ((let uu___12 = + FStar_TypeChecker_Env.debug + env.FStar_SMTEncoding_Env.tcenv + (FStar_Options.Other "SMTEncoding") in + if uu___12 + then + let uu___13 = + FStar_Ident.string_of_lid t in + FStar_Compiler_Util.print2 + "%s injectivity for %s\n" + (if is_injective_on_params + then "YES" + else "NO") uu___13 + else ()); + is_injective_on_params)))))) +let (encode_sig_inductive : + Prims.bool -> + FStar_SMTEncoding_Env.env_t -> + FStar_Syntax_Syntax.sigelt -> + (FStar_SMTEncoding_Term.decls_t * FStar_SMTEncoding_Env.env_t)) = - fun env -> - fun se -> - (let uu___1 = - FStar_TypeChecker_Env.debug env.FStar_SMTEncoding_Env.tcenv - (FStar_Options.Other "SMTEncoding") in - if uu___1 - then - let uu___2 = FStar_Syntax_Print.sigelt_to_string se in - FStar_Compiler_Util.print1 "@@@Encoding sigelt %s\n" uu___2 - else ()); - (let is_opaque_to_smt t = - let uu___1 = - let uu___2 = FStar_Syntax_Subst.compress t in - uu___2.FStar_Syntax_Syntax.n in - match uu___1 with - | FStar_Syntax_Syntax.Tm_constant (FStar_Const.Const_string - (s, uu___2)) -> s = "opaque_to_smt" - | uu___2 -> false in - let is_uninterpreted_by_smt t = - let uu___1 = - let uu___2 = FStar_Syntax_Subst.compress t in - uu___2.FStar_Syntax_Syntax.n in - match uu___1 with - | FStar_Syntax_Syntax.Tm_constant (FStar_Const.Const_string - (s, uu___2)) -> s = "uninterpreted_by_smt" - | uu___2 -> false in - match se.FStar_Syntax_Syntax.sigel with - | FStar_Syntax_Syntax.Sig_splice uu___1 -> - FStar_Compiler_Effect.failwith - "impossible -- splice should have been removed by Tc.fs" - | FStar_Syntax_Syntax.Sig_fail uu___1 -> - FStar_Compiler_Effect.failwith - "impossible -- Sig_fail should have been removed by Tc.fs" - | FStar_Syntax_Syntax.Sig_pragma uu___1 -> ([], env) - | FStar_Syntax_Syntax.Sig_effect_abbrev uu___1 -> ([], env) - | FStar_Syntax_Syntax.Sig_sub_effect uu___1 -> ([], env) - | FStar_Syntax_Syntax.Sig_polymonadic_bind uu___1 -> ([], env) - | FStar_Syntax_Syntax.Sig_polymonadic_subcomp uu___1 -> ([], env) - | FStar_Syntax_Syntax.Sig_new_effect ed -> - let uu___1 = - let uu___2 = - FStar_SMTEncoding_Util.is_smt_reifiable_effect - env.FStar_SMTEncoding_Env.tcenv ed.FStar_Syntax_Syntax.mname in - Prims.op_Negation uu___2 in - if uu___1 - then ([], env) - else - (let close_effect_params tm = - match ed.FStar_Syntax_Syntax.binders with - | [] -> tm - | uu___3 -> - FStar_Syntax_Syntax.mk - (FStar_Syntax_Syntax.Tm_abs - { - FStar_Syntax_Syntax.bs = - (ed.FStar_Syntax_Syntax.binders); - FStar_Syntax_Syntax.body = tm; - FStar_Syntax_Syntax.rc_opt = - (FStar_Pervasives_Native.Some - (FStar_Syntax_Util.mk_residual_comp - FStar_Parser_Const.effect_Tot_lid - FStar_Pervasives_Native.None - [FStar_Syntax_Syntax.TOTAL])) - }) tm.FStar_Syntax_Syntax.pos in - let encode_action env1 a = - let action_defn = - let uu___3 = - close_effect_params a.FStar_Syntax_Syntax.action_defn in - norm_before_encoding env1 uu___3 in + fun is_injective_on_params -> + fun env -> + fun se -> + let uu___ = se.FStar_Syntax_Syntax.sigel in + match uu___ with + | FStar_Syntax_Syntax.Sig_inductive_typ + { FStar_Syntax_Syntax.lid = t; + FStar_Syntax_Syntax.us = universe_names; + FStar_Syntax_Syntax.params = tps; + FStar_Syntax_Syntax.num_uniform_params = uu___1; + FStar_Syntax_Syntax.t = k; + FStar_Syntax_Syntax.mutuals = uu___2; + FStar_Syntax_Syntax.ds = datas;_} + -> + let t_lid = t in + let tcenv = env.FStar_SMTEncoding_Env.tcenv in + let quals = se.FStar_Syntax_Syntax.sigquals in + let is_logical = + FStar_Compiler_Util.for_some + (fun uu___3 -> + match uu___3 with + | FStar_Syntax_Syntax.Logic -> true + | FStar_Syntax_Syntax.Assumption -> true + | uu___4 -> false) quals in + let constructor_or_logic_type_decl c = + if is_logical + then let uu___3 = - FStar_Syntax_Util.arrow_formals_comp - a.FStar_Syntax_Syntax.action_typ in - match uu___3 with - | (formals, uu___4) -> - let arity = FStar_Compiler_List.length formals in + let uu___4 = let uu___5 = - FStar_SMTEncoding_Env.new_term_constant_and_tok_from_lid - env1 a.FStar_Syntax_Syntax.action_name arity in - (match uu___5 with - | (aname, atok, env2) -> - let uu___6 = - FStar_SMTEncoding_EncodeTerm.encode_term - action_defn env2 in - (match uu___6 with - | (tm, decls) -> - let a_decls = - let uu___7 = + FStar_Compiler_List.map + (fun f -> f.FStar_SMTEncoding_Term.field_sort) + c.FStar_SMTEncoding_Term.constr_fields in + ((c.FStar_SMTEncoding_Term.constr_name), uu___5, + FStar_SMTEncoding_Term.Term_sort, + FStar_Pervasives_Native.None) in + FStar_SMTEncoding_Term.DeclFun uu___4 in + [uu___3] + else + (let uu___4 = FStar_Ident.range_of_lid t in + FStar_SMTEncoding_Term.constructor_to_decl uu___4 c) in + let inversion_axioms env1 tapp vars = + let uu___3 = + FStar_Compiler_Util.for_some + (fun l -> + let uu___4 = + FStar_TypeChecker_Env.try_lookup_lid + env1.FStar_SMTEncoding_Env.tcenv l in + FStar_Compiler_Option.isNone uu___4) datas in + if uu___3 + then [] + else + (let uu___5 = + FStar_SMTEncoding_Env.fresh_fvar + env1.FStar_SMTEncoding_Env.current_module_name "x" + FStar_SMTEncoding_Term.Term_sort in + match uu___5 with + | (xxsym, xx) -> + let uu___6 = + FStar_Compiler_List.fold_left + (fun uu___7 -> + fun l -> + match uu___7 with + | (out, decls) -> let uu___8 = - let uu___9 = - FStar_Compiler_List.map - (fun uu___10 -> - FStar_SMTEncoding_Term.Term_sort) - formals in - (aname, uu___9, - FStar_SMTEncoding_Term.Term_sort, - (FStar_Pervasives_Native.Some "Action")) in - FStar_SMTEncoding_Term.DeclFun uu___8 in - [uu___7; - FStar_SMTEncoding_Term.DeclFun - (atok, [], - FStar_SMTEncoding_Term.Term_sort, - (FStar_Pervasives_Native.Some - "Action token"))] in - let uu___7 = - let aux uu___8 uu___9 = - match (uu___8, uu___9) with - | ({ FStar_Syntax_Syntax.binder_bv = bv; - FStar_Syntax_Syntax.binder_qual = - uu___10; - FStar_Syntax_Syntax.binder_positivity - = uu___11; - FStar_Syntax_Syntax.binder_attrs = - uu___12;_}, - (env3, acc_sorts, acc)) -> - let uu___13 = - FStar_SMTEncoding_Env.gen_term_var - env3 bv in - (match uu___13 with - | (xxsym, xx, env4) -> - let uu___14 = - let uu___15 = - FStar_SMTEncoding_Term.mk_fv - (xxsym, - FStar_SMTEncoding_Term.Term_sort) in - uu___15 :: acc_sorts in - (env4, uu___14, (xx :: acc))) in - FStar_Compiler_List.fold_right aux formals - (env2, [], []) in - (match uu___7 with - | (uu___8, xs_sorts, xs) -> - let app = - FStar_SMTEncoding_Util.mkApp (aname, xs) in - let a_eq = - let uu___9 = + FStar_TypeChecker_Env.lookup_datacon + env1.FStar_SMTEncoding_Env.tcenv l in + (match uu___8 with + | (uu___9, data_t) -> let uu___10 = - let uu___11 = - FStar_Ident.range_of_lid - a.FStar_Syntax_Syntax.action_name in - let uu___12 = - let uu___13 = - let uu___14 = - let uu___15 = - FStar_SMTEncoding_EncodeTerm.mk_Apply - tm xs_sorts in - (app, uu___15) in - FStar_SMTEncoding_Util.mkEq - uu___14 in - ([[app]], xs_sorts, uu___13) in - FStar_SMTEncoding_Term.mkForall - uu___11 uu___12 in - (uu___10, - (FStar_Pervasives_Native.Some - "Action equality"), - (Prims.strcat aname "_equality")) in - FStar_SMTEncoding_Util.mkAssume uu___9 in - let tok_correspondence = - let tok_term = - let uu___9 = - FStar_SMTEncoding_Term.mk_fv - (atok, - FStar_SMTEncoding_Term.Term_sort) in - FStar_SMTEncoding_Util.mkFreeV uu___9 in - let tok_app = - FStar_SMTEncoding_EncodeTerm.mk_Apply - tok_term xs_sorts in - let uu___9 = - let uu___10 = - let uu___11 = - FStar_Ident.range_of_lid - a.FStar_Syntax_Syntax.action_name in - let uu___12 = - let uu___13 = - FStar_SMTEncoding_Util.mkEq - (tok_app, app) in - ([[tok_app]], xs_sorts, uu___13) in - FStar_SMTEncoding_Term.mkForall - uu___11 uu___12 in - (uu___10, - (FStar_Pervasives_Native.Some - "Action token correspondence"), - (Prims.strcat aname - "_token_correspondence")) in - FStar_SMTEncoding_Util.mkAssume uu___9 in + FStar_Syntax_Util.arrow_formals + data_t in + (match uu___10 with + | (args, res) -> + let indices = + let uu___11 = + FStar_Syntax_Util.head_and_args_full + res in + FStar_Pervasives_Native.snd + uu___11 in + let env2 = + FStar_Compiler_List.fold_left + (fun env3 -> + fun uu___11 -> + match uu___11 with + | { + FStar_Syntax_Syntax.binder_bv + = x; + FStar_Syntax_Syntax.binder_qual + = uu___12; + FStar_Syntax_Syntax.binder_positivity + = uu___13; + FStar_Syntax_Syntax.binder_attrs + = uu___14;_} + -> + let uu___15 = + let uu___16 = + let uu___17 = + FStar_SMTEncoding_Env.mk_term_projector_name + l x in + (uu___17, [xx]) in + FStar_SMTEncoding_Util.mkApp + uu___16 in + FStar_SMTEncoding_Env.push_term_var + env3 x uu___15) + env1 args in + let uu___11 = + FStar_SMTEncoding_EncodeTerm.encode_args + indices env2 in + (match uu___11 with + | (indices1, decls') -> + (if + (FStar_Compiler_List.length + indices1) + <> + (FStar_Compiler_List.length + vars) + then + FStar_Compiler_Effect.failwith + "Impossible" + else (); + (let eqs = + let uu___13 = + is_injective_on_params + || + (let uu___14 = + FStar_Options.ext_getv + "compat:injectivity" in + uu___14 <> "") in + if uu___13 + then + FStar_Compiler_List.map2 + (fun v -> + fun a -> + let uu___14 = + let uu___15 = + FStar_SMTEncoding_Util.mkFreeV + v in + (uu___15, a) in + FStar_SMTEncoding_Util.mkEq + uu___14) vars + indices1 + else + (let num_params = + FStar_Compiler_List.length + tps in + let uu___15 = + FStar_Compiler_List.splitAt + num_params vars in + match uu___15 with + | (_var_params, + var_indices) -> + let uu___16 = + FStar_Compiler_List.splitAt + num_params + indices1 in + (match uu___16 + with + | (_i_params, + indices2) -> + FStar_Compiler_List.map2 + (fun v -> + fun a -> + let uu___17 + = + let uu___18 + = + FStar_SMTEncoding_Util.mkFreeV + v in + (uu___18, + a) in + FStar_SMTEncoding_Util.mkEq + uu___17) + var_indices + indices2)) in + let uu___13 = + let uu___14 = + let uu___15 = + let uu___16 = + let uu___17 = + FStar_SMTEncoding_Env.mk_data_tester + env2 l xx in + let uu___18 = + FStar_SMTEncoding_Util.mk_and_l + eqs in + (uu___17, uu___18) in + FStar_SMTEncoding_Util.mkAnd + uu___16 in + (out, uu___15) in + FStar_SMTEncoding_Util.mkOr + uu___14 in + (uu___13, + (FStar_Compiler_List.op_At + decls decls')))))))) + (FStar_SMTEncoding_Util.mkFalse, []) datas in + (match uu___6 with + | (data_ax, decls) -> + let uu___7 = + FStar_SMTEncoding_Env.fresh_fvar + env1.FStar_SMTEncoding_Env.current_module_name + "f" FStar_SMTEncoding_Term.Fuel_sort in + (match uu___7 with + | (ffsym, ff) -> + let fuel_guarded_inversion = + let xx_has_type_sfuel = + if + (FStar_Compiler_List.length datas) > + Prims.int_one + then + let uu___8 = + FStar_SMTEncoding_Util.mkApp + ("SFuel", [ff]) in + FStar_SMTEncoding_Term.mk_HasTypeFuel + uu___8 xx tapp + else + FStar_SMTEncoding_Term.mk_HasTypeFuel ff + xx tapp in + let uu___8 = let uu___9 = - let uu___10 = - FStar_SMTEncoding_Term.mk_decls_trivial - (FStar_Compiler_List.op_At a_decls - [a_eq; tok_correspondence]) in - FStar_Compiler_List.op_At decls uu___10 in - (env2, uu___9)))) in - let uu___3 = - FStar_Compiler_Util.fold_map encode_action env - ed.FStar_Syntax_Syntax.actions in - match uu___3 with - | (env1, decls2) -> - ((FStar_Compiler_List.flatten decls2), env1)) - | FStar_Syntax_Syntax.Sig_declare_typ - { FStar_Syntax_Syntax.lid2 = lid; - FStar_Syntax_Syntax.us2 = uu___1; - FStar_Syntax_Syntax.t2 = uu___2;_} - when FStar_Ident.lid_equals lid FStar_Parser_Const.precedes_lid -> - let uu___3 = - FStar_SMTEncoding_Env.new_term_constant_and_tok_from_lid env lid - (Prims.of_int (4)) in - (match uu___3 with | (tname, ttok, env1) -> ([], env1)) - | FStar_Syntax_Syntax.Sig_declare_typ - { FStar_Syntax_Syntax.lid2 = lid; - FStar_Syntax_Syntax.us2 = uu___1; FStar_Syntax_Syntax.t2 = t;_} - -> - let quals = se.FStar_Syntax_Syntax.sigquals in - let will_encode_definition = - let uu___2 = - FStar_Compiler_Util.for_some - (fun uu___3 -> - match uu___3 with - | FStar_Syntax_Syntax.Assumption -> true - | FStar_Syntax_Syntax.Projector uu___4 -> true - | FStar_Syntax_Syntax.Discriminator uu___4 -> true - | FStar_Syntax_Syntax.Irreducible -> true - | uu___4 -> false) quals in - Prims.op_Negation uu___2 in - if will_encode_definition - then ([], env) - else - (let fv = - FStar_Syntax_Syntax.lid_as_fv lid - FStar_Pervasives_Native.None in - let uu___3 = - let uu___4 = - FStar_Compiler_Util.for_some is_uninterpreted_by_smt - se.FStar_Syntax_Syntax.sigattrs in - encode_top_level_val uu___4 env fv t quals in - match uu___3 with - | (decls, env1) -> - let tname = FStar_Ident.string_of_lid lid in - let tsym = - let uu___4 = - FStar_SMTEncoding_Env.try_lookup_free_var env1 lid in - FStar_Compiler_Option.get uu___4 in - let uu___4 = + let uu___10 = FStar_Ident.range_of_lid t in + let uu___11 = + let uu___12 = + let uu___13 = + FStar_SMTEncoding_Term.mk_fv + (ffsym, + FStar_SMTEncoding_Term.Fuel_sort) in + let uu___14 = + let uu___15 = + FStar_SMTEncoding_Term.mk_fv + (xxsym, + FStar_SMTEncoding_Term.Term_sort) in + uu___15 :: vars in + FStar_SMTEncoding_Env.add_fuel + uu___13 uu___14 in + let uu___13 = + FStar_SMTEncoding_Util.mkImp + (xx_has_type_sfuel, data_ax) in + ([[xx_has_type_sfuel]], uu___12, + uu___13) in + FStar_SMTEncoding_Term.mkForall uu___10 + uu___11 in + let uu___10 = + let uu___11 = + let uu___12 = + FStar_Ident.string_of_lid t in + Prims.strcat "fuel_guarded_inversion_" + uu___12 in + FStar_SMTEncoding_Env.varops.FStar_SMTEncoding_Env.mk_unique + uu___11 in + (uu___9, + (FStar_Pervasives_Native.Some + "inversion axiom"), uu___10) in + FStar_SMTEncoding_Util.mkAssume uu___8 in + let uu___8 = + FStar_SMTEncoding_Term.mk_decls_trivial + [fuel_guarded_inversion] in + FStar_Compiler_List.op_At decls uu___8))) in + let uu___3 = + let k1 = + match tps with + | [] -> k + | uu___4 -> let uu___5 = let uu___6 = - primitive_type_axioms - env1.FStar_SMTEncoding_Env.tcenv lid tname tsym in - FStar_SMTEncoding_Term.mk_decls_trivial uu___6 in - FStar_Compiler_List.op_At decls uu___5 in - (uu___4, env1)) - | FStar_Syntax_Syntax.Sig_assume - { FStar_Syntax_Syntax.lid3 = l; FStar_Syntax_Syntax.us3 = us; - FStar_Syntax_Syntax.phi1 = f;_} - -> - let uu___1 = FStar_Syntax_Subst.open_univ_vars us f in - (match uu___1 with - | (uvs, f1) -> - let env1 = - let uu___2 = - FStar_TypeChecker_Env.push_univ_vars - env.FStar_SMTEncoding_Env.tcenv uvs in - { - FStar_SMTEncoding_Env.bvar_bindings = - (env.FStar_SMTEncoding_Env.bvar_bindings); - FStar_SMTEncoding_Env.fvar_bindings = - (env.FStar_SMTEncoding_Env.fvar_bindings); - FStar_SMTEncoding_Env.depth = - (env.FStar_SMTEncoding_Env.depth); - FStar_SMTEncoding_Env.tcenv = uu___2; - FStar_SMTEncoding_Env.warn = - (env.FStar_SMTEncoding_Env.warn); - FStar_SMTEncoding_Env.nolabels = - (env.FStar_SMTEncoding_Env.nolabels); - FStar_SMTEncoding_Env.use_zfuel_name = - (env.FStar_SMTEncoding_Env.use_zfuel_name); - FStar_SMTEncoding_Env.encode_non_total_function_typ = - (env.FStar_SMTEncoding_Env.encode_non_total_function_typ); - FStar_SMTEncoding_Env.current_module_name = - (env.FStar_SMTEncoding_Env.current_module_name); - FStar_SMTEncoding_Env.encoding_quantifier = - (env.FStar_SMTEncoding_Env.encoding_quantifier); - FStar_SMTEncoding_Env.global_cache = - (env.FStar_SMTEncoding_Env.global_cache) - } in - let f2 = norm_before_encoding env1 f1 in - let uu___2 = - FStar_SMTEncoding_EncodeTerm.encode_formula f2 env1 in - (match uu___2 with - | (f3, decls) -> - let g = - let uu___3 = - let uu___4 = - let uu___5 = - let uu___6 = - let uu___7 = - let uu___8 = - FStar_Syntax_Print.lid_to_string l in - FStar_Compiler_Util.format1 "Assumption: %s" - uu___8 in - FStar_Pervasives_Native.Some uu___7 in - let uu___7 = - let uu___8 = - let uu___9 = FStar_Ident.string_of_lid l in - Prims.strcat "assumption_" uu___9 in - FStar_SMTEncoding_Env.varops.FStar_SMTEncoding_Env.mk_unique - uu___8 in - (f3, uu___6, uu___7) in - FStar_SMTEncoding_Util.mkAssume uu___5 in - [uu___4] in - FStar_SMTEncoding_Term.mk_decls_trivial uu___3 in - ((FStar_Compiler_List.op_At decls g), env1))) - | FStar_Syntax_Syntax.Sig_let - { FStar_Syntax_Syntax.lbs1 = lbs; - FStar_Syntax_Syntax.lids1 = uu___1;_} - when - (FStar_Compiler_List.contains FStar_Syntax_Syntax.Irreducible - se.FStar_Syntax_Syntax.sigquals) - || - (FStar_Compiler_Util.for_some is_opaque_to_smt - se.FStar_Syntax_Syntax.sigattrs) - -> - let attrs = se.FStar_Syntax_Syntax.sigattrs in - let uu___2 = - FStar_Compiler_Util.fold_map - (fun env1 -> - fun lb -> - let lid = - let uu___3 = - let uu___4 = - FStar_Compiler_Util.right - lb.FStar_Syntax_Syntax.lbname in - uu___4.FStar_Syntax_Syntax.fv_name in - uu___3.FStar_Syntax_Syntax.v in - let uu___3 = - let uu___4 = - FStar_TypeChecker_Env.try_lookup_val_decl - env1.FStar_SMTEncoding_Env.tcenv lid in - FStar_Compiler_Option.isNone uu___4 in - if uu___3 - then - let val_decl = + let uu___7 = FStar_Syntax_Syntax.mk_Total k in { - FStar_Syntax_Syntax.sigel = - (FStar_Syntax_Syntax.Sig_declare_typ - { - FStar_Syntax_Syntax.lid2 = lid; - FStar_Syntax_Syntax.us2 = - (lb.FStar_Syntax_Syntax.lbunivs); - FStar_Syntax_Syntax.t2 = - (lb.FStar_Syntax_Syntax.lbtyp) - }); - FStar_Syntax_Syntax.sigrng = - (se.FStar_Syntax_Syntax.sigrng); - FStar_Syntax_Syntax.sigquals = - (FStar_Syntax_Syntax.Irreducible :: - (se.FStar_Syntax_Syntax.sigquals)); - FStar_Syntax_Syntax.sigmeta = - (se.FStar_Syntax_Syntax.sigmeta); - FStar_Syntax_Syntax.sigattrs = - (se.FStar_Syntax_Syntax.sigattrs); - FStar_Syntax_Syntax.sigopens_and_abbrevs = - (se.FStar_Syntax_Syntax.sigopens_and_abbrevs); - FStar_Syntax_Syntax.sigopts = - (se.FStar_Syntax_Syntax.sigopts) + FStar_Syntax_Syntax.bs1 = tps; + FStar_Syntax_Syntax.comp = uu___7 } in - let uu___4 = encode_sigelt' env1 val_decl in - match uu___4 with | (decls, env2) -> (env2, decls) - else (env1, [])) env (FStar_Pervasives_Native.snd lbs) in - (match uu___2 with - | (env1, decls) -> ((FStar_Compiler_List.flatten decls), env1)) - | FStar_Syntax_Syntax.Sig_let - { - FStar_Syntax_Syntax.lbs1 = - (uu___1, - { FStar_Syntax_Syntax.lbname = FStar_Pervasives.Inr b2t; - FStar_Syntax_Syntax.lbunivs = uu___2; - FStar_Syntax_Syntax.lbtyp = uu___3; - FStar_Syntax_Syntax.lbeff = uu___4; - FStar_Syntax_Syntax.lbdef = uu___5; - FStar_Syntax_Syntax.lbattrs = uu___6; - FStar_Syntax_Syntax.lbpos = uu___7;_}::[]); - FStar_Syntax_Syntax.lids1 = uu___8;_} - when FStar_Syntax_Syntax.fv_eq_lid b2t FStar_Parser_Const.b2t_lid - -> - let uu___9 = - FStar_SMTEncoding_Env.new_term_constant_and_tok_from_lid env - (b2t.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v - Prims.int_one in - (match uu___9 with - | (tname, ttok, env1) -> - let xx = - FStar_SMTEncoding_Term.mk_fv - ("x", FStar_SMTEncoding_Term.Term_sort) in - let x = FStar_SMTEncoding_Util.mkFreeV xx in - let b2t_x = FStar_SMTEncoding_Util.mkApp ("Prims.b2t", [x]) in - let valid_b2t_x = - FStar_SMTEncoding_Util.mkApp ("Valid", [b2t_x]) in - let bool_ty = - let uu___10 = - FStar_Syntax_Syntax.withsort FStar_Parser_Const.bool_lid in - FStar_SMTEncoding_Env.lookup_free_var env1 uu___10 in - let decls = - let uu___10 = - let uu___11 = - let uu___12 = - let uu___13 = - let uu___14 = FStar_Syntax_Syntax.range_of_fv b2t in - let uu___15 = - let uu___16 = - let uu___17 = - let uu___18 = - FStar_SMTEncoding_Util.mkApp - ((FStar_Pervasives_Native.snd - FStar_SMTEncoding_Term.boxBoolFun), - [x]) in - (valid_b2t_x, uu___18) in - FStar_SMTEncoding_Util.mkEq uu___17 in - ([[b2t_x]], [xx], uu___16) in - FStar_SMTEncoding_Term.mkForall uu___14 uu___15 in - (uu___13, (FStar_Pervasives_Native.Some "b2t def"), - "b2t_def") in - FStar_SMTEncoding_Util.mkAssume uu___12 in - let uu___12 = - let uu___13 = - let uu___14 = - let uu___15 = - let uu___16 = FStar_Syntax_Syntax.range_of_fv b2t in - let uu___17 = - let uu___18 = - let uu___19 = - let uu___20 = - FStar_SMTEncoding_Term.mk_HasType x - bool_ty in - let uu___21 = - FStar_SMTEncoding_Term.mk_HasType b2t_x - FStar_SMTEncoding_Term.mk_Term_type in - (uu___20, uu___21) in - FStar_SMTEncoding_Util.mkImp uu___19 in - ([[b2t_x]], [xx], uu___18) in - FStar_SMTEncoding_Term.mkForall uu___16 uu___17 in - (uu___15, - (FStar_Pervasives_Native.Some "b2t typing"), - "b2t_typing") in - FStar_SMTEncoding_Util.mkAssume uu___14 in - [uu___13] in - uu___11 :: uu___12 in - (FStar_SMTEncoding_Term.DeclFun - (tname, [FStar_SMTEncoding_Term.Term_sort], - FStar_SMTEncoding_Term.Term_sort, - FStar_Pervasives_Native.None)) - :: uu___10 in - let uu___10 = FStar_SMTEncoding_Term.mk_decls_trivial decls in - (uu___10, env1)) - | FStar_Syntax_Syntax.Sig_let uu___1 when - FStar_Compiler_Util.for_some - (fun uu___2 -> - match uu___2 with - | FStar_Syntax_Syntax.Discriminator uu___3 -> true - | uu___3 -> false) se.FStar_Syntax_Syntax.sigquals - -> - ((let uu___3 = - FStar_TypeChecker_Env.debug env.FStar_SMTEncoding_Env.tcenv - (FStar_Options.Other "SMTEncoding") in - if uu___3 - then - let uu___4 = FStar_Syntax_Print.sigelt_to_string_short se in - FStar_Compiler_Util.print1 "Not encoding discriminator '%s'\n" - uu___4 - else ()); - ([], env)) - | FStar_Syntax_Syntax.Sig_let - { FStar_Syntax_Syntax.lbs1 = uu___1; - FStar_Syntax_Syntax.lids1 = lids;_} - when - (FStar_Compiler_Util.for_some - (fun l -> - let uu___2 = - let uu___3 = - let uu___4 = FStar_Ident.ns_of_lid l in - FStar_Compiler_List.hd uu___4 in - FStar_Ident.string_of_id uu___3 in - uu___2 = "Prims") lids) - && - (FStar_Compiler_Util.for_some - (fun uu___2 -> - match uu___2 with - | FStar_Syntax_Syntax.Unfold_for_unification_and_vcgen -> - true - | uu___3 -> false) se.FStar_Syntax_Syntax.sigquals) - -> - ((let uu___3 = - FStar_TypeChecker_Env.debug env.FStar_SMTEncoding_Env.tcenv - (FStar_Options.Other "SMTEncoding") in - if uu___3 - then - let uu___4 = FStar_Syntax_Print.sigelt_to_string_short se in - FStar_Compiler_Util.print1 - "Not encoding unfold let from Prims '%s'\n" uu___4 - else ()); - ([], env)) - | FStar_Syntax_Syntax.Sig_let - { FStar_Syntax_Syntax.lbs1 = (false, lb::[]); - FStar_Syntax_Syntax.lids1 = uu___1;_} - when - FStar_Compiler_Util.for_some - (fun uu___2 -> - match uu___2 with - | FStar_Syntax_Syntax.Projector uu___3 -> true - | uu___3 -> false) se.FStar_Syntax_Syntax.sigquals - -> - let fv = FStar_Compiler_Util.right lb.FStar_Syntax_Syntax.lbname in - let l = (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in - let uu___2 = FStar_SMTEncoding_Env.try_lookup_free_var env l in - (match uu___2 with - | FStar_Pervasives_Native.Some uu___3 -> ([], env) - | FStar_Pervasives_Native.None -> - let se1 = - let uu___3 = FStar_Ident.range_of_lid l in - { - FStar_Syntax_Syntax.sigel = - (FStar_Syntax_Syntax.Sig_declare_typ - { - FStar_Syntax_Syntax.lid2 = l; - FStar_Syntax_Syntax.us2 = - (lb.FStar_Syntax_Syntax.lbunivs); - FStar_Syntax_Syntax.t2 = - (lb.FStar_Syntax_Syntax.lbtyp) - }); - FStar_Syntax_Syntax.sigrng = uu___3; - FStar_Syntax_Syntax.sigquals = - (se.FStar_Syntax_Syntax.sigquals); - FStar_Syntax_Syntax.sigmeta = - (se.FStar_Syntax_Syntax.sigmeta); - FStar_Syntax_Syntax.sigattrs = - (se.FStar_Syntax_Syntax.sigattrs); - FStar_Syntax_Syntax.sigopens_and_abbrevs = - (se.FStar_Syntax_Syntax.sigopens_and_abbrevs); - FStar_Syntax_Syntax.sigopts = - (se.FStar_Syntax_Syntax.sigopts) - } in - encode_sigelt env se1) - | FStar_Syntax_Syntax.Sig_let - { FStar_Syntax_Syntax.lbs1 = (is_rec, bindings); - FStar_Syntax_Syntax.lids1 = uu___1;_} - -> - let bindings1 = - FStar_Compiler_List.map - (fun lb -> - let def = - norm_before_encoding env lb.FStar_Syntax_Syntax.lbdef in - let typ = - norm_before_encoding env lb.FStar_Syntax_Syntax.lbtyp in - { - FStar_Syntax_Syntax.lbname = - (lb.FStar_Syntax_Syntax.lbname); - FStar_Syntax_Syntax.lbunivs = - (lb.FStar_Syntax_Syntax.lbunivs); - FStar_Syntax_Syntax.lbtyp = typ; - FStar_Syntax_Syntax.lbeff = - (lb.FStar_Syntax_Syntax.lbeff); - FStar_Syntax_Syntax.lbdef = def; - FStar_Syntax_Syntax.lbattrs = - (lb.FStar_Syntax_Syntax.lbattrs); - FStar_Syntax_Syntax.lbpos = - (lb.FStar_Syntax_Syntax.lbpos) - }) bindings in - encode_top_level_let env (is_rec, bindings1) - se.FStar_Syntax_Syntax.sigquals - | FStar_Syntax_Syntax.Sig_bundle - { FStar_Syntax_Syntax.ses = ses; - FStar_Syntax_Syntax.lids = uu___1;_} - -> - let uu___2 = encode_sigelts env ses in - (match uu___2 with - | (g, env1) -> - let uu___3 = - FStar_Compiler_List.fold_left - (fun uu___4 -> - fun elt -> - match uu___4 with - | (g', inversions) -> - let uu___5 = - FStar_Compiler_List.partition - (fun uu___6 -> - match uu___6 with - | FStar_SMTEncoding_Term.Assume - { - FStar_SMTEncoding_Term.assumption_term - = uu___7; - FStar_SMTEncoding_Term.assumption_caption - = FStar_Pervasives_Native.Some - "inversion axiom"; - FStar_SMTEncoding_Term.assumption_name - = uu___8; - FStar_SMTEncoding_Term.assumption_fact_ids - = uu___9;_} - -> false - | uu___7 -> true) - elt.FStar_SMTEncoding_Term.decls in - (match uu___5 with - | (elt_g', elt_inversions) -> - ((FStar_Compiler_List.op_At g' - [{ - FStar_SMTEncoding_Term.sym_name = - (elt.FStar_SMTEncoding_Term.sym_name); - FStar_SMTEncoding_Term.key = - (elt.FStar_SMTEncoding_Term.key); - FStar_SMTEncoding_Term.decls = - elt_g'; - FStar_SMTEncoding_Term.a_names = - (elt.FStar_SMTEncoding_Term.a_names) - }]), - (FStar_Compiler_List.op_At inversions - elt_inversions)))) ([], []) g in - (match uu___3 with - | (g', inversions) -> - let uu___4 = - FStar_Compiler_List.fold_left - (fun uu___5 -> - fun elt -> - match uu___5 with - | (decls, elts, rest) -> - let uu___6 = - (FStar_Compiler_Util.is_some - elt.FStar_SMTEncoding_Term.key) - && - (FStar_Compiler_List.existsb - (fun uu___7 -> - match uu___7 with - | FStar_SMTEncoding_Term.DeclFun - uu___8 -> true - | uu___8 -> false) - elt.FStar_SMTEncoding_Term.decls) in - if uu___6 - then - (decls, - (FStar_Compiler_List.op_At elts [elt]), - rest) - else - (let uu___8 = - FStar_Compiler_List.partition - (fun uu___9 -> - match uu___9 with - | FStar_SMTEncoding_Term.DeclFun - uu___10 -> true - | uu___10 -> false) - elt.FStar_SMTEncoding_Term.decls in - match uu___8 with - | (elt_decls, elt_rest) -> - ((FStar_Compiler_List.op_At decls - elt_decls), elts, - (FStar_Compiler_List.op_At rest - [{ - FStar_SMTEncoding_Term.sym_name - = - (elt.FStar_SMTEncoding_Term.sym_name); - FStar_SMTEncoding_Term.key = - (elt.FStar_SMTEncoding_Term.key); - FStar_SMTEncoding_Term.decls - = elt_rest; - FStar_SMTEncoding_Term.a_names - = - (elt.FStar_SMTEncoding_Term.a_names) - }])))) ([], [], []) g' in - (match uu___4 with - | (decls, elts, rest) -> - let uu___5 = - let uu___6 = - FStar_SMTEncoding_Term.mk_decls_trivial decls in - let uu___7 = - let uu___8 = - let uu___9 = - FStar_SMTEncoding_Term.mk_decls_trivial - inversions in - FStar_Compiler_List.op_At rest uu___9 in - FStar_Compiler_List.op_At elts uu___8 in - FStar_Compiler_List.op_At uu___6 uu___7 in - (uu___5, env1)))) - | FStar_Syntax_Syntax.Sig_inductive_typ - { FStar_Syntax_Syntax.lid = t; - FStar_Syntax_Syntax.us = universe_names; - FStar_Syntax_Syntax.params = tps; - FStar_Syntax_Syntax.num_uniform_params = uu___1; - FStar_Syntax_Syntax.t = k; FStar_Syntax_Syntax.mutuals = uu___2; - FStar_Syntax_Syntax.ds = datas;_} - -> - let t_lid = t in - let tcenv = env.FStar_SMTEncoding_Env.tcenv in - let is_injective_on_params = - let uu___3 = FStar_Syntax_Subst.univ_var_opening universe_names in - match uu___3 with - | (usubst, uvs) -> - let uu___4 = - let uu___5 = - FStar_TypeChecker_Env.push_univ_vars tcenv uvs in - let uu___6 = FStar_Syntax_Subst.subst_binders usubst tps in - let uu___7 = - let uu___8 = - FStar_Syntax_Subst.shift_subst - (FStar_Compiler_List.length tps) usubst in - FStar_Syntax_Subst.subst uu___8 k in - (uu___5, uu___6, uu___7) in - (match uu___4 with - | (env1, tps1, k1) -> - let uu___5 = FStar_Syntax_Subst.open_term tps1 k1 in - (match uu___5 with - | (tps2, k2) -> - let uu___6 = FStar_Syntax_Util.arrow_formals k2 in - (match uu___6 with - | (uu___7, k3) -> - let uu___8 = - FStar_TypeChecker_TcTerm.tc_binders env1 - tps2 in - (match uu___8 with - | (tps3, env_tps, uu___9, us) -> - let u_k = - let uu___10 = - let uu___11 = - FStar_Syntax_Syntax.fvar t - FStar_Pervasives_Native.None in - let uu___12 = - let uu___13 = - FStar_Syntax_Util.args_of_binders - tps3 in - FStar_Pervasives_Native.snd - uu___13 in - let uu___13 = - FStar_Ident.range_of_lid t in - FStar_Syntax_Syntax.mk_Tm_app - uu___11 uu___12 uu___13 in - FStar_TypeChecker_TcTerm.level_of_type - env_tps uu___10 k3 in - let rec universe_leq u v = - match (u, v) with - | (FStar_Syntax_Syntax.U_zero, - uu___10) -> true - | (FStar_Syntax_Syntax.U_succ u0, - FStar_Syntax_Syntax.U_succ v0) -> - universe_leq u0 v0 - | (FStar_Syntax_Syntax.U_name u0, - FStar_Syntax_Syntax.U_name v0) -> - FStar_Ident.ident_equals u0 v0 - | (FStar_Syntax_Syntax.U_name uu___10, - FStar_Syntax_Syntax.U_succ v0) -> - universe_leq u v0 - | (FStar_Syntax_Syntax.U_max us1, - uu___10) -> - FStar_Compiler_Util.for_all - (fun u1 -> universe_leq u1 v) - us1 - | (uu___10, FStar_Syntax_Syntax.U_max - vs) -> - FStar_Compiler_Util.for_some - (universe_leq u) vs - | (FStar_Syntax_Syntax.U_unknown, - uu___10) -> - let uu___11 = - let uu___12 = - FStar_Ident.string_of_lid t in - let uu___13 = - FStar_Syntax_Print.univ_to_string - u in - let uu___14 = - FStar_Syntax_Print.univ_to_string - v in - FStar_Compiler_Util.format3 - "Impossible: Unresolved or unknown universe in inductive type %s (%s, %s)" - uu___12 uu___13 uu___14 in - FStar_Compiler_Effect.failwith - uu___11 - | (uu___10, - FStar_Syntax_Syntax.U_unknown) -> - let uu___11 = - let uu___12 = - FStar_Ident.string_of_lid t in - let uu___13 = - FStar_Syntax_Print.univ_to_string - u in - let uu___14 = - FStar_Syntax_Print.univ_to_string - v in - FStar_Compiler_Util.format3 - "Impossible: Unresolved or unknown universe in inductive type %s (%s, %s)" - uu___12 uu___13 uu___14 in - FStar_Compiler_Effect.failwith - uu___11 - | (FStar_Syntax_Syntax.U_unif uu___10, - uu___11) -> - let uu___12 = - let uu___13 = - FStar_Ident.string_of_lid t in - let uu___14 = - FStar_Syntax_Print.univ_to_string - u in - let uu___15 = - FStar_Syntax_Print.univ_to_string - v in - FStar_Compiler_Util.format3 - "Impossible: Unresolved or unknown universe in inductive type %s (%s, %s)" - uu___13 uu___14 uu___15 in - FStar_Compiler_Effect.failwith - uu___12 - | (uu___10, FStar_Syntax_Syntax.U_unif - uu___11) -> - let uu___12 = - let uu___13 = - FStar_Ident.string_of_lid t in - let uu___14 = - FStar_Syntax_Print.univ_to_string - u in - let uu___15 = - FStar_Syntax_Print.univ_to_string - v in - FStar_Compiler_Util.format3 - "Impossible: Unresolved or unknown universe in inductive type %s (%s, %s)" - uu___13 uu___14 uu___15 in - FStar_Compiler_Effect.failwith - uu___12 - | uu___10 -> false in - let u_leq_u_k u = - let u1 = - FStar_TypeChecker_Normalize.normalize_universe - env_tps u in - universe_leq u1 u_k in - let tp_ok tp u_tp = - let t_tp = - (tp.FStar_Syntax_Syntax.binder_bv).FStar_Syntax_Syntax.sort in - let uu___10 = u_leq_u_k u_tp in - if uu___10 - then true - else - (let t_tp1 = - FStar_TypeChecker_Normalize.normalize - [FStar_TypeChecker_Env.Unrefine; - FStar_TypeChecker_Env.Unascribe; - FStar_TypeChecker_Env.Unmeta; - FStar_TypeChecker_Env.Primops; - FStar_TypeChecker_Env.HNF; - FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Beta] - env_tps t_tp in - let uu___12 = - FStar_Syntax_Util.arrow_formals - t_tp1 in - match uu___12 with - | (formals, t1) -> - let uu___13 = - FStar_TypeChecker_TcTerm.tc_binders - env_tps formals in - (match uu___13 with - | (uu___14, uu___15, uu___16, - u_formals) -> - let inj = - FStar_Compiler_Util.for_all - (fun u_formal -> - u_leq_u_k u_formal) - u_formals in - if inj - then - let uu___17 = - let uu___18 = - FStar_Syntax_Subst.compress - t1 in - uu___18.FStar_Syntax_Syntax.n in - (match uu___17 with - | FStar_Syntax_Syntax.Tm_type - u -> u_leq_u_k u - | uu___18 -> false) - else false)) in - FStar_Compiler_List.forall2 tp_ok tps3 - us)))) in - ((let uu___4 = - FStar_TypeChecker_Env.debug env.FStar_SMTEncoding_Env.tcenv - (FStar_Options.Other "SMTEncoding") in - if uu___4 - then - let uu___5 = FStar_Ident.string_of_lid t in - FStar_Compiler_Util.print2 "%s injectivity for %s\n" - (if is_injective_on_params then "YES" else "NO") uu___5 - else ()); - (let quals = se.FStar_Syntax_Syntax.sigquals in - let is_logical = - FStar_Compiler_Util.for_some - (fun uu___4 -> - match uu___4 with - | FStar_Syntax_Syntax.Logic -> true - | FStar_Syntax_Syntax.Assumption -> true - | uu___5 -> false) quals in - let constructor_or_logic_type_decl c = - if is_logical - then - let uu___4 = - let uu___5 = - let uu___6 = - FStar_Compiler_List.map - (fun f -> f.FStar_SMTEncoding_Term.field_sort) - c.FStar_SMTEncoding_Term.constr_fields in - ((c.FStar_SMTEncoding_Term.constr_name), uu___6, - FStar_SMTEncoding_Term.Term_sort, - FStar_Pervasives_Native.None) in - FStar_SMTEncoding_Term.DeclFun uu___5 in - [uu___4] - else - (let uu___5 = FStar_Ident.range_of_lid t in - FStar_SMTEncoding_Term.constructor_to_decl uu___5 c) in - let inversion_axioms env1 tapp vars = - let uu___4 = - FStar_Compiler_Util.for_some - (fun l -> - let uu___5 = - FStar_TypeChecker_Env.try_lookup_lid - env1.FStar_SMTEncoding_Env.tcenv l in - FStar_Compiler_Option.isNone uu___5) datas in - if uu___4 - then [] - else - (let uu___6 = - FStar_SMTEncoding_Env.fresh_fvar - env1.FStar_SMTEncoding_Env.current_module_name "x" - FStar_SMTEncoding_Term.Term_sort in - match uu___6 with - | (xxsym, xx) -> - let uu___7 = - FStar_Compiler_List.fold_left - (fun uu___8 -> - fun l -> - match uu___8 with - | (out, decls) -> - let uu___9 = - FStar_TypeChecker_Env.lookup_datacon - env1.FStar_SMTEncoding_Env.tcenv l in - (match uu___9 with - | (uu___10, data_t) -> - let uu___11 = - FStar_Syntax_Util.arrow_formals - data_t in - (match uu___11 with - | (args, res) -> - let indices = - let uu___12 = - FStar_Syntax_Util.head_and_args_full - res in - FStar_Pervasives_Native.snd - uu___12 in - let env2 = - FStar_Compiler_List.fold_left - (fun env3 -> - fun uu___12 -> - match uu___12 with - | { - FStar_Syntax_Syntax.binder_bv - = x; - FStar_Syntax_Syntax.binder_qual - = uu___13; - FStar_Syntax_Syntax.binder_positivity - = uu___14; - FStar_Syntax_Syntax.binder_attrs - = uu___15;_} - -> - let uu___16 = - let uu___17 = - let uu___18 = - FStar_SMTEncoding_Env.mk_term_projector_name - l x in - (uu___18, [xx]) in - FStar_SMTEncoding_Util.mkApp - uu___17 in - FStar_SMTEncoding_Env.push_term_var - env3 x uu___16) - env1 args in - let uu___12 = - FStar_SMTEncoding_EncodeTerm.encode_args - indices env2 in - (match uu___12 with - | (indices1, decls') -> - (if - (FStar_Compiler_List.length - indices1) - <> - (FStar_Compiler_List.length - vars) - then - FStar_Compiler_Effect.failwith - "Impossible" - else (); - (let eqs = - let uu___14 = - is_injective_on_params - || - (let uu___15 = - FStar_Options.ext_getv - "compat:injectivity" in - uu___15 <> "") in - if uu___14 - then - FStar_Compiler_List.map2 - (fun v -> - fun a -> - let uu___15 = - let uu___16 - = - FStar_SMTEncoding_Util.mkFreeV - v in - (uu___16, a) in - FStar_SMTEncoding_Util.mkEq - uu___15) - vars indices1 - else - (let num_params = - FStar_Compiler_List.length - tps in - let uu___16 = - FStar_Compiler_List.splitAt - num_params vars in - match uu___16 with - | (_var_params, - var_indices) -> - let uu___17 = - FStar_Compiler_List.splitAt - num_params - indices1 in - (match uu___17 - with - | (_i_params, - indices2) -> - FStar_Compiler_List.map2 - ( - fun v -> - fun a -> - let uu___18 - = - let uu___19 - = - FStar_SMTEncoding_Util.mkFreeV - v in - (uu___19, - a) in - FStar_SMTEncoding_Util.mkEq - uu___18) - var_indices - indices2)) in - let uu___14 = - let uu___15 = - let uu___16 = - let uu___17 = - let uu___18 = - FStar_SMTEncoding_Env.mk_data_tester - env2 l xx in - let uu___19 = - FStar_SMTEncoding_Util.mk_and_l - eqs in - (uu___18, - uu___19) in - FStar_SMTEncoding_Util.mkAnd - uu___17 in - (out, uu___16) in - FStar_SMTEncoding_Util.mkOr - uu___15 in - (uu___14, - (FStar_Compiler_List.op_At - decls decls')))))))) - (FStar_SMTEncoding_Util.mkFalse, []) datas in - (match uu___7 with - | (data_ax, decls) -> - let uu___8 = - FStar_SMTEncoding_Env.fresh_fvar - env1.FStar_SMTEncoding_Env.current_module_name - "f" FStar_SMTEncoding_Term.Fuel_sort in - (match uu___8 with - | (ffsym, ff) -> - let fuel_guarded_inversion = - let xx_has_type_sfuel = - if - (FStar_Compiler_List.length datas) > - Prims.int_one - then - let uu___9 = - FStar_SMTEncoding_Util.mkApp - ("SFuel", [ff]) in - FStar_SMTEncoding_Term.mk_HasTypeFuel - uu___9 xx tapp - else - FStar_SMTEncoding_Term.mk_HasTypeFuel - ff xx tapp in - let uu___9 = - let uu___10 = - let uu___11 = - FStar_Ident.range_of_lid t in - let uu___12 = - let uu___13 = - let uu___14 = - FStar_SMTEncoding_Term.mk_fv - (ffsym, - FStar_SMTEncoding_Term.Fuel_sort) in - let uu___15 = - let uu___16 = - FStar_SMTEncoding_Term.mk_fv - (xxsym, - FStar_SMTEncoding_Term.Term_sort) in - uu___16 :: vars in - FStar_SMTEncoding_Env.add_fuel - uu___14 uu___15 in - let uu___14 = - FStar_SMTEncoding_Util.mkImp - (xx_has_type_sfuel, data_ax) in - ([[xx_has_type_sfuel]], uu___13, - uu___14) in - FStar_SMTEncoding_Term.mkForall uu___11 - uu___12 in - let uu___11 = - let uu___12 = - let uu___13 = - FStar_Ident.string_of_lid t in - Prims.strcat - "fuel_guarded_inversion_" uu___13 in - FStar_SMTEncoding_Env.varops.FStar_SMTEncoding_Env.mk_unique - uu___12 in - (uu___10, - (FStar_Pervasives_Native.Some - "inversion axiom"), uu___11) in - FStar_SMTEncoding_Util.mkAssume uu___9 in - let uu___9 = - FStar_SMTEncoding_Term.mk_decls_trivial - [fuel_guarded_inversion] in - FStar_Compiler_List.op_At decls uu___9))) in - let uu___4 = - let k1 = - match tps with - | [] -> k - | uu___5 -> - let uu___6 = - let uu___7 = - let uu___8 = FStar_Syntax_Syntax.mk_Total k in - { - FStar_Syntax_Syntax.bs1 = tps; - FStar_Syntax_Syntax.comp = uu___8 - } in - FStar_Syntax_Syntax.Tm_arrow uu___7 in - FStar_Syntax_Syntax.mk uu___6 k.FStar_Syntax_Syntax.pos in - let k2 = norm_before_encoding env k1 in - FStar_Syntax_Util.arrow_formals k2 in - match uu___4 with - | (formals, res) -> - let uu___5 = - FStar_SMTEncoding_EncodeTerm.encode_binders - FStar_Pervasives_Native.None formals env in - (match uu___5 with - | (vars, guards, env', binder_decls, uu___6) -> - let arity = FStar_Compiler_List.length vars in - let uu___7 = - FStar_SMTEncoding_Env.new_term_constant_and_tok_from_lid - env t arity in - (match uu___7 with - | (tname, ttok, env1) -> - let ttok_tm = - FStar_SMTEncoding_Util.mkApp (ttok, []) in - let guard = FStar_SMTEncoding_Util.mk_and_l guards in - let tapp = - let uu___8 = - let uu___9 = - FStar_Compiler_List.map - FStar_SMTEncoding_Util.mkFreeV vars in - (tname, uu___9) in - FStar_SMTEncoding_Util.mkApp uu___8 in - let uu___8 = - let tname_decl = - let uu___9 = - let uu___10 = - FStar_Compiler_List.map - (fun fv -> - let uu___11 = - let uu___12 = - FStar_SMTEncoding_Term.fv_name fv in - Prims.strcat tname uu___12 in - let uu___12 = - FStar_SMTEncoding_Term.fv_sort fv in + FStar_Syntax_Syntax.Tm_arrow uu___6 in + FStar_Syntax_Syntax.mk uu___5 k.FStar_Syntax_Syntax.pos in + let k2 = norm_before_encoding env k1 in + FStar_Syntax_Util.arrow_formals k2 in + (match uu___3 with + | (formals, res) -> + let uu___4 = + FStar_SMTEncoding_EncodeTerm.encode_binders + FStar_Pervasives_Native.None formals env in + (match uu___4 with + | (vars, guards, env', binder_decls, uu___5) -> + let arity = FStar_Compiler_List.length vars in + let uu___6 = + FStar_SMTEncoding_Env.new_term_constant_and_tok_from_lid + env t arity in + (match uu___6 with + | (tname, ttok, env1) -> + let ttok_tm = + FStar_SMTEncoding_Util.mkApp (ttok, []) in + let guard = FStar_SMTEncoding_Util.mk_and_l guards in + let tapp = + let uu___7 = + let uu___8 = + FStar_Compiler_List.map + FStar_SMTEncoding_Util.mkFreeV vars in + (tname, uu___8) in + FStar_SMTEncoding_Util.mkApp uu___7 in + let uu___7 = + let tname_decl = + let uu___8 = + let uu___9 = + FStar_Compiler_List.map + (fun fv -> + let uu___10 = + let uu___11 = + FStar_SMTEncoding_Term.fv_name fv in + Prims.strcat tname uu___11 in + let uu___11 = + FStar_SMTEncoding_Term.fv_sort fv in { FStar_SMTEncoding_Term.field_name = - uu___11; + uu___10; FStar_SMTEncoding_Term.field_sort = - uu___12; + uu___11; FStar_SMTEncoding_Term.field_projectible = false }) vars in - let uu___11 = - let uu___12 = + let uu___10 = + let uu___11 = FStar_SMTEncoding_Env.varops.FStar_SMTEncoding_Env.next_id () in - FStar_Pervasives_Native.Some uu___12 in + FStar_Pervasives_Native.Some uu___11 in { FStar_SMTEncoding_Term.constr_name = tname; FStar_SMTEncoding_Term.constr_fields = - uu___10; + uu___9; FStar_SMTEncoding_Term.constr_sort = FStar_SMTEncoding_Term.Term_sort; - FStar_SMTEncoding_Term.constr_id = uu___11 + FStar_SMTEncoding_Term.constr_id = uu___10 } in - constructor_or_logic_type_decl uu___9 in - let uu___9 = + constructor_or_logic_type_decl uu___8 in + let uu___8 = match vars with | [] -> - let uu___10 = - let uu___11 = - let uu___12 = + let uu___9 = + let uu___10 = + let uu___11 = FStar_SMTEncoding_Util.mkApp (tname, []) in - FStar_Pervasives_Native.Some uu___12 in + FStar_Pervasives_Native.Some uu___11 in FStar_SMTEncoding_Env.push_free_var env1 - t arity tname uu___11 in - ([], uu___10) - | uu___10 -> + t arity tname uu___10 in + ([], uu___9) + | uu___9 -> let ttok_decl = FStar_SMTEncoding_Term.DeclFun (ttok, [], @@ -5037,328 +4329,342 @@ and (encode_sigelt' : (FStar_Pervasives_Native.Some "token")) in let ttok_fresh = - let uu___11 = + let uu___10 = FStar_SMTEncoding_Env.varops.FStar_SMTEncoding_Env.next_id () in FStar_SMTEncoding_Term.fresh_token (ttok, FStar_SMTEncoding_Term.Term_sort) - uu___11 in + uu___10 in let ttok_app = FStar_SMTEncoding_EncodeTerm.mk_Apply ttok_tm vars in let pats = [[ttok_app]; [tapp]] in let name_tok_corr = - let uu___11 = - let uu___12 = - let uu___13 = + let uu___10 = + let uu___11 = + let uu___12 = FStar_Ident.range_of_lid t in - let uu___14 = - let uu___15 = + let uu___13 = + let uu___14 = FStar_SMTEncoding_Util.mkEq (ttok_app, tapp) in (pats, FStar_Pervasives_Native.None, - vars, uu___15) in + vars, uu___14) in FStar_SMTEncoding_Term.mkForall' - uu___13 uu___14 in - (uu___12, + uu___12 uu___13 in + (uu___11, (FStar_Pervasives_Native.Some "name-token correspondence"), (Prims.strcat "token_correspondence_" ttok)) in - FStar_SMTEncoding_Util.mkAssume uu___11 in + FStar_SMTEncoding_Util.mkAssume uu___10 in ([ttok_decl; ttok_fresh; name_tok_corr], env1) in - match uu___9 with + match uu___8 with | (tok_decls, env2) -> ((FStar_Compiler_List.op_At tname_decl tok_decls), env2) in - (match uu___8 with + (match uu___7 with | (decls, env2) -> let kindingAx = - let uu___9 = + let uu___8 = FStar_SMTEncoding_EncodeTerm.encode_term_pred FStar_Pervasives_Native.None res env' tapp in - match uu___9 with + match uu___8 with | (k1, decls1) -> let karr = if (FStar_Compiler_List.length formals) > Prims.int_zero then - let uu___10 = - let uu___11 = - let uu___12 = - let uu___13 = + let uu___9 = + let uu___10 = + let uu___11 = + let uu___12 = FStar_SMTEncoding_Term.mk_PreType ttok_tm in FStar_SMTEncoding_Term.mk_tester - "Tm_arrow" uu___13 in - (uu___12, + "Tm_arrow" uu___12 in + (uu___11, (FStar_Pervasives_Native.Some "kinding"), (Prims.strcat "pre_kinding_" ttok)) in FStar_SMTEncoding_Util.mkAssume - uu___11 in - [uu___10] + uu___10 in + [uu___9] else [] in let rng = FStar_Ident.range_of_lid t in let tot_fun_axioms = - let uu___10 = + let uu___9 = FStar_Compiler_List.map - (fun uu___11 -> + (fun uu___10 -> FStar_SMTEncoding_Util.mkTrue) vars in FStar_SMTEncoding_EncodeTerm.isTotFun_axioms - rng ttok_tm vars uu___10 true in - let uu___10 = - let uu___11 = - let uu___12 = - let uu___13 = - let uu___14 = - let uu___15 = - let uu___16 = - let uu___17 = - let uu___18 = - let uu___19 = + rng ttok_tm vars uu___9 true in + let uu___9 = + let uu___10 = + let uu___11 = + let uu___12 = + let uu___13 = + let uu___14 = + let uu___15 = + let uu___16 = + let uu___17 = + let uu___18 = FStar_SMTEncoding_Util.mkImp (guard, k1) in ([[tapp]], vars, - uu___19) in + uu___18) in FStar_SMTEncoding_Term.mkForall - rng uu___18 in - (tot_fun_axioms, uu___17) in + rng uu___17 in + (tot_fun_axioms, uu___16) in FStar_SMTEncoding_Util.mkAnd - uu___16 in - (uu___15, + uu___15 in + (uu___14, FStar_Pervasives_Native.None, (Prims.strcat "kinding_" ttok)) in FStar_SMTEncoding_Util.mkAssume - uu___14 in - [uu___13] in + uu___13 in + [uu___12] in FStar_Compiler_List.op_At karr - uu___12 in + uu___11 in FStar_SMTEncoding_Term.mk_decls_trivial - uu___11 in - FStar_Compiler_List.op_At decls1 - uu___10 in + uu___10 in + FStar_Compiler_List.op_At decls1 uu___9 in let aux = - let uu___9 = - let uu___10 = + let uu___8 = + let uu___9 = inversion_axioms env2 tapp vars in - let uu___11 = - let uu___12 = - let uu___13 = - let uu___14 = + let uu___10 = + let uu___11 = + let uu___12 = + let uu___13 = FStar_Ident.range_of_lid t in - pretype_axiom uu___14 env2 tapp + pretype_axiom uu___13 env2 tapp vars in - [uu___13] in + [uu___12] in FStar_SMTEncoding_Term.mk_decls_trivial - uu___12 in - FStar_Compiler_List.op_At uu___10 uu___11 in - FStar_Compiler_List.op_At kindingAx uu___9 in - let g = + uu___11 in + FStar_Compiler_List.op_At uu___9 uu___10 in + FStar_Compiler_List.op_At kindingAx uu___8 in + let uu___8 = let uu___9 = FStar_SMTEncoding_Term.mk_decls_trivial decls in FStar_Compiler_List.op_At uu___9 (FStar_Compiler_List.op_At binder_decls aux) in - (g, env2)))))) - | FStar_Syntax_Syntax.Sig_datacon - { FStar_Syntax_Syntax.lid1 = d; FStar_Syntax_Syntax.us1 = uu___1; - FStar_Syntax_Syntax.t1 = t; FStar_Syntax_Syntax.ty_lid = uu___2; - FStar_Syntax_Syntax.num_ty_params = n_tps; - FStar_Syntax_Syntax.mutuals1 = mutuals;_} - -> - let quals = se.FStar_Syntax_Syntax.sigquals in - let t1 = norm_before_encoding env t in - let uu___3 = FStar_Syntax_Util.arrow_formals t1 in - (match uu___3 with - | (formals, t_res) -> - let arity = FStar_Compiler_List.length formals in - let uu___4 = - FStar_SMTEncoding_Env.new_term_constant_and_tok_from_lid - env d arity in - (match uu___4 with - | (ddconstrsym, ddtok, env1) -> - let ddtok_tm = FStar_SMTEncoding_Util.mkApp (ddtok, []) in - let uu___5 = - FStar_SMTEncoding_Env.fresh_fvar - env1.FStar_SMTEncoding_Env.current_module_name "f" - FStar_SMTEncoding_Term.Fuel_sort in - (match uu___5 with - | (fuel_var, fuel_tm) -> - let s_fuel_tm = - FStar_SMTEncoding_Util.mkApp ("SFuel", [fuel_tm]) in - let uu___6 = - FStar_SMTEncoding_EncodeTerm.encode_binders - (FStar_Pervasives_Native.Some fuel_tm) formals - env1 in - (match uu___6 with - | (vars, guards, env', binder_decls, names) -> - let fields = - FStar_Compiler_List.mapi - (fun n -> - fun x -> - let uu___7 = - FStar_SMTEncoding_Env.mk_term_projector_name - d x in - { - FStar_SMTEncoding_Term.field_name = - uu___7; - FStar_SMTEncoding_Term.field_sort = - FStar_SMTEncoding_Term.Term_sort; - FStar_SMTEncoding_Term.field_projectible - = true - }) names in - let datacons = - let uu___7 = FStar_Ident.range_of_lid d in - let uu___8 = - let uu___9 = - let uu___10 = - FStar_SMTEncoding_Env.varops.FStar_SMTEncoding_Env.next_id - () in - FStar_Pervasives_Native.Some uu___10 in - { - FStar_SMTEncoding_Term.constr_name = - ddconstrsym; - FStar_SMTEncoding_Term.constr_fields = - fields; - FStar_SMTEncoding_Term.constr_sort = - FStar_SMTEncoding_Term.Term_sort; - FStar_SMTEncoding_Term.constr_id = - uu___9 - } in - FStar_SMTEncoding_Term.constructor_to_decl - uu___7 uu___8 in - let app = - FStar_SMTEncoding_EncodeTerm.mk_Apply - ddtok_tm vars in - let guard = - FStar_SMTEncoding_Util.mk_and_l guards in - let xvars = - FStar_Compiler_List.map - FStar_SMTEncoding_Util.mkFreeV vars in - let dapp = - FStar_SMTEncoding_Util.mkApp - (ddconstrsym, xvars) in - let uu___7 = - FStar_SMTEncoding_EncodeTerm.encode_term_pred - FStar_Pervasives_Native.None t1 env1 - ddtok_tm in - (match uu___7 with - | (tok_typing, decls3) -> - let tok_typing1 = - match fields with - | uu___8::uu___9 -> - let ff = - FStar_SMTEncoding_Term.mk_fv - ("ty", - FStar_SMTEncoding_Term.Term_sort) in - let f = - FStar_SMTEncoding_Util.mkFreeV ff in - let vtok_app_l = - FStar_SMTEncoding_EncodeTerm.mk_Apply - ddtok_tm [ff] in - let vtok_app_r = - let uu___10 = - let uu___11 = - FStar_SMTEncoding_Term.mk_fv - (ddtok, - FStar_SMTEncoding_Term.Term_sort) in - [uu___11] in - FStar_SMTEncoding_EncodeTerm.mk_Apply - f uu___10 in - let uu___10 = - FStar_Ident.range_of_lid d in - let uu___11 = - let uu___12 = - FStar_SMTEncoding_Term.mk_NoHoist - f tok_typing in - ([[vtok_app_l]; [vtok_app_r]], - [ff], uu___12) in - FStar_SMTEncoding_Term.mkForall - uu___10 uu___11 - | uu___8 -> tok_typing in - let uu___8 = - let uu___9 = - FStar_SMTEncoding_EncodeTerm.encode_term - t_res env' in - match uu___9 with - | (t_res_tm, t_res_decls) -> - let uu___10 = - FStar_SMTEncoding_Term.mk_HasTypeWithFuel - (FStar_Pervasives_Native.Some - fuel_tm) dapp t_res_tm in - (uu___10, t_res_tm, t_res_decls) in - (match uu___8 with - | (ty_pred', t_res_tm, decls_pred) -> - let proxy_fresh = - match formals with - | [] -> [] - | uu___9 -> - let uu___10 = - let uu___11 = - FStar_SMTEncoding_Env.varops.FStar_SMTEncoding_Env.next_id - () in - FStar_SMTEncoding_Term.fresh_token - (ddtok, - FStar_SMTEncoding_Term.Term_sort) - uu___11 in - [uu___10] in - let encode_elim uu___9 = - let uu___10 = - FStar_Syntax_Util.head_and_args - t_res in - match uu___10 with - | (head, args) -> - let uu___11 = - let uu___12 = - FStar_Syntax_Subst.compress - head in - uu___12.FStar_Syntax_Syntax.n in - (match uu___11 with - | FStar_Syntax_Syntax.Tm_uinst - ({ - FStar_Syntax_Syntax.n - = - FStar_Syntax_Syntax.Tm_fvar - fv; - FStar_Syntax_Syntax.pos - = uu___12; - FStar_Syntax_Syntax.vars - = uu___13; - FStar_Syntax_Syntax.hash_code - = uu___14;_}, - uu___15) - -> - let encoded_head_fvb = - FStar_SMTEncoding_Env.lookup_free_var_name - env' - fv.FStar_Syntax_Syntax.fv_name in - let uu___16 = - FStar_SMTEncoding_EncodeTerm.encode_args - args env' in - (match uu___16 with - | (encoded_args, - arg_decls) -> - let guards_for_parameter - orig_arg arg xv = - let fv1 = - match arg.FStar_SMTEncoding_Term.tm - with - | FStar_SMTEncoding_Term.FreeV - fv2 -> fv2 - | uu___17 -> - let uu___18 - = - let uu___19 + (uu___8, env2))))) +let (encode_datacon : + Prims.bool -> + FStar_SMTEncoding_Env.env_t -> + FStar_Syntax_Syntax.sigelt -> + (FStar_SMTEncoding_Term.decls_t * FStar_SMTEncoding_Env.env_t)) + = + fun is_injective_on_tparams -> + fun env -> + fun se -> + let uu___ = se.FStar_Syntax_Syntax.sigel in + match uu___ with + | FStar_Syntax_Syntax.Sig_datacon + { FStar_Syntax_Syntax.lid1 = d; FStar_Syntax_Syntax.us1 = uu___1; + FStar_Syntax_Syntax.t1 = t; + FStar_Syntax_Syntax.ty_lid = uu___2; + FStar_Syntax_Syntax.num_ty_params = n_tps; + FStar_Syntax_Syntax.mutuals1 = mutuals;_} + -> + let quals = se.FStar_Syntax_Syntax.sigquals in + let t1 = norm_before_encoding env t in + let uu___3 = FStar_Syntax_Util.arrow_formals t1 in + (match uu___3 with + | (formals, t_res) -> + let arity = FStar_Compiler_List.length formals in + let uu___4 = + FStar_SMTEncoding_Env.new_term_constant_and_tok_from_lid + env d arity in + (match uu___4 with + | (ddconstrsym, ddtok, env1) -> + let ddtok_tm = FStar_SMTEncoding_Util.mkApp (ddtok, []) in + let uu___5 = + FStar_SMTEncoding_Env.fresh_fvar + env1.FStar_SMTEncoding_Env.current_module_name "f" + FStar_SMTEncoding_Term.Fuel_sort in + (match uu___5 with + | (fuel_var, fuel_tm) -> + let s_fuel_tm = + FStar_SMTEncoding_Util.mkApp + ("SFuel", [fuel_tm]) in + let uu___6 = + FStar_SMTEncoding_EncodeTerm.encode_binders + (FStar_Pervasives_Native.Some fuel_tm) formals + env1 in + (match uu___6 with + | (vars, guards, env', binder_decls, names) -> + let fields = + FStar_Compiler_List.mapi + (fun n -> + fun x -> + let uu___7 = + FStar_SMTEncoding_Env.mk_term_projector_name + d x in + { + FStar_SMTEncoding_Term.field_name + = uu___7; + FStar_SMTEncoding_Term.field_sort + = + FStar_SMTEncoding_Term.Term_sort; + FStar_SMTEncoding_Term.field_projectible + = true + }) names in + let datacons = + let uu___7 = FStar_Ident.range_of_lid d in + let uu___8 = + let uu___9 = + let uu___10 = + FStar_SMTEncoding_Env.varops.FStar_SMTEncoding_Env.next_id + () in + FStar_Pervasives_Native.Some uu___10 in + { + FStar_SMTEncoding_Term.constr_name = + ddconstrsym; + FStar_SMTEncoding_Term.constr_fields = + fields; + FStar_SMTEncoding_Term.constr_sort = + FStar_SMTEncoding_Term.Term_sort; + FStar_SMTEncoding_Term.constr_id = + uu___9 + } in + FStar_SMTEncoding_Term.constructor_to_decl + uu___7 uu___8 in + let app = + FStar_SMTEncoding_EncodeTerm.mk_Apply + ddtok_tm vars in + let guard = + FStar_SMTEncoding_Util.mk_and_l guards in + let xvars = + FStar_Compiler_List.map + FStar_SMTEncoding_Util.mkFreeV vars in + let dapp = + FStar_SMTEncoding_Util.mkApp + (ddconstrsym, xvars) in + let uu___7 = + FStar_SMTEncoding_EncodeTerm.encode_term_pred + FStar_Pervasives_Native.None t1 env1 + ddtok_tm in + (match uu___7 with + | (tok_typing, decls3) -> + let tok_typing1 = + match fields with + | uu___8::uu___9 -> + let ff = + FStar_SMTEncoding_Term.mk_fv + ("ty", + FStar_SMTEncoding_Term.Term_sort) in + let f = + FStar_SMTEncoding_Util.mkFreeV + ff in + let vtok_app_l = + FStar_SMTEncoding_EncodeTerm.mk_Apply + ddtok_tm [ff] in + let vtok_app_r = + let uu___10 = + let uu___11 = + FStar_SMTEncoding_Term.mk_fv + (ddtok, + FStar_SMTEncoding_Term.Term_sort) in + [uu___11] in + FStar_SMTEncoding_EncodeTerm.mk_Apply + f uu___10 in + let uu___10 = + FStar_Ident.range_of_lid d in + let uu___11 = + let uu___12 = + FStar_SMTEncoding_Term.mk_NoHoist + f tok_typing in + ([[vtok_app_l]; [vtok_app_r]], + [ff], uu___12) in + FStar_SMTEncoding_Term.mkForall + uu___10 uu___11 + | uu___8 -> tok_typing in + let uu___8 = + let uu___9 = + FStar_SMTEncoding_EncodeTerm.encode_term + t_res env' in + match uu___9 with + | (t_res_tm, t_res_decls) -> + let uu___10 = + FStar_SMTEncoding_Term.mk_HasTypeWithFuel + (FStar_Pervasives_Native.Some + fuel_tm) dapp t_res_tm in + (uu___10, t_res_tm, t_res_decls) in + (match uu___8 with + | (ty_pred', t_res_tm, decls_pred) -> + let proxy_fresh = + match formals with + | [] -> [] + | uu___9 -> + let uu___10 = + let uu___11 = + FStar_SMTEncoding_Env.varops.FStar_SMTEncoding_Env.next_id + () in + FStar_SMTEncoding_Term.fresh_token + (ddtok, + FStar_SMTEncoding_Term.Term_sort) + uu___11 in + [uu___10] in + let encode_elim uu___9 = + let uu___10 = + FStar_Syntax_Util.head_and_args + t_res in + match uu___10 with + | (head, args) -> + let uu___11 = + let uu___12 = + FStar_Syntax_Subst.compress + head in + uu___12.FStar_Syntax_Syntax.n in + (match uu___11 with + | FStar_Syntax_Syntax.Tm_uinst + ({ + FStar_Syntax_Syntax.n + = + FStar_Syntax_Syntax.Tm_fvar + fv; + FStar_Syntax_Syntax.pos + = uu___12; + FStar_Syntax_Syntax.vars + = uu___13; + FStar_Syntax_Syntax.hash_code + = uu___14;_}, + uu___15) + -> + let encoded_head_fvb = + FStar_SMTEncoding_Env.lookup_free_var_name + env' + fv.FStar_Syntax_Syntax.fv_name in + let uu___16 = + FStar_SMTEncoding_EncodeTerm.encode_args + args env' in + (match uu___16 with + | (encoded_args, + arg_decls) -> + let guards_for_parameter + orig_arg arg xv = + let fv1 = + match arg.FStar_SMTEncoding_Term.tm + with + | FStar_SMTEncoding_Term.FreeV + fv2 -> fv2 + | uu___17 -> + let uu___18 + = + let uu___19 = let uu___20 = @@ -5367,15 +4673,15 @@ and (encode_sigelt' : FStar_Compiler_Util.format1 "Inductive type parameter %s must be a variable ; You may want to change it to an index." uu___20 in - (FStar_Errors_Codes.Fatal_NonVariableInductiveTypeParameter, + (FStar_Errors_Codes.Fatal_NonVariableInductiveTypeParameter, uu___19) in - FStar_Errors.raise_error - uu___18 - orig_arg.FStar_Syntax_Syntax.pos in - let guards1 = - FStar_Compiler_List.collect - (fun g -> - let uu___17 + FStar_Errors.raise_error + uu___18 + orig_arg.FStar_Syntax_Syntax.pos in + let guards1 = + FStar_Compiler_List.collect + (fun g -> + let uu___17 = let uu___18 = @@ -5384,31 +4690,32 @@ and (encode_sigelt' : FStar_Compiler_List.contains fv1 uu___18 in - if uu___17 - then + if uu___17 + then let uu___18 = FStar_SMTEncoding_Term.subst g fv1 xv in [uu___18] - else []) - guards in - FStar_SMTEncoding_Util.mk_and_l - guards1 in - let uu___17 = - let uu___18 = - FStar_Compiler_List.zip - args - encoded_args in - FStar_Compiler_List.fold_left - (fun uu___19 -> - fun uu___20 - -> - match + else []) + guards in + FStar_SMTEncoding_Util.mk_and_l + guards1 in + let uu___17 = + let uu___18 = + FStar_Compiler_List.zip + args + encoded_args in + FStar_Compiler_List.fold_left + (fun uu___19 -> + fun uu___20 + -> + match (uu___19, uu___20) - with - | ((env2, + with + | + ((env2, arg_vars, eqns_or_guards, i), @@ -5458,44 +4765,46 @@ and (encode_sigelt' : eqns, (i + Prims.int_one)))) - (env', [], [], - Prims.int_zero) - uu___18 in - (match uu___17 with - | (uu___18, - arg_vars, - elim_eqns_or_guards, - uu___19) -> - let arg_vars1 = - FStar_Compiler_List.rev - arg_vars in - let ty = - FStar_SMTEncoding_EncodeTerm.maybe_curry_fvb - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.p - encoded_head_fvb - arg_vars1 in - let xvars1 = - FStar_Compiler_List.map - FStar_SMTEncoding_Util.mkFreeV - vars in - let dapp1 = - FStar_SMTEncoding_Util.mkApp - (ddconstrsym, + (env', [], [], + Prims.int_zero) + uu___18 in + (match uu___17 with + | (uu___18, + arg_vars, + elim_eqns_or_guards, + uu___19) -> + let arg_vars1 + = + FStar_Compiler_List.rev + arg_vars in + let ty = + FStar_SMTEncoding_EncodeTerm.maybe_curry_fvb + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.p + encoded_head_fvb + arg_vars1 in + let xvars1 = + FStar_Compiler_List.map + FStar_SMTEncoding_Util.mkFreeV + vars in + let dapp1 = + FStar_SMTEncoding_Util.mkApp + (ddconstrsym, xvars1) in - let ty_pred = - FStar_SMTEncoding_Term.mk_HasTypeWithFuel - (FStar_Pervasives_Native.Some + let ty_pred = + FStar_SMTEncoding_Term.mk_HasTypeWithFuel + (FStar_Pervasives_Native.Some s_fuel_tm) - dapp1 ty in - let arg_binders - = - FStar_Compiler_List.map - FStar_SMTEncoding_Term.fv_of_term - arg_vars1 in - let typing_inversion - = - let uu___20 = - let uu___21 + dapp1 ty in + let arg_binders + = + FStar_Compiler_List.map + FStar_SMTEncoding_Term.fv_of_term + arg_vars1 in + let typing_inversion + = + let uu___20 + = + let uu___21 = let uu___22 = @@ -5536,19 +4845,18 @@ and (encode_sigelt' : FStar_SMTEncoding_Term.mkForall uu___22 uu___23 in - (uu___21, - ( - FStar_Pervasives_Native.Some + (uu___21, + (FStar_Pervasives_Native.Some "data constructor typing elim"), - ( - Prims.strcat + (Prims.strcat "data_elim_" ddconstrsym)) in - FStar_SMTEncoding_Util.mkAssume - uu___20 in - let lex_t = - let uu___20 = - let uu___21 + FStar_SMTEncoding_Util.mkAssume + uu___20 in + let lex_t = + let uu___20 + = + let uu___21 = let uu___22 = @@ -5556,14 +4864,14 @@ and (encode_sigelt' : FStar_Parser_Const.lex_t_lid in (uu___22, FStar_SMTEncoding_Term.Term_sort) in - FStar_SMTEncoding_Term.mk_fv + FStar_SMTEncoding_Term.mk_fv uu___21 in - FStar_SMTEncoding_Util.mkFreeV - uu___20 in - let subterm_ordering - = - let prec = - let uu___20 + FStar_SMTEncoding_Util.mkFreeV + uu___20 in + let subterm_ordering + = + let prec = + let uu___20 = FStar_Compiler_List.mapi (fun i -> @@ -5585,10 +4893,11 @@ and (encode_sigelt' : dapp1 in [uu___22])) vars in - FStar_Compiler_List.flatten + FStar_Compiler_List.flatten uu___20 in - let uu___20 = - let uu___21 + let uu___20 + = + let uu___21 = let uu___22 = @@ -5627,25 +4936,24 @@ and (encode_sigelt' : FStar_SMTEncoding_Term.mkForall uu___22 uu___23 in - (uu___21, - ( - FStar_Pervasives_Native.Some + (uu___21, + (FStar_Pervasives_Native.Some "subterm ordering"), - ( - Prims.strcat + (Prims.strcat "subterm_ordering_" ddconstrsym)) in - FStar_SMTEncoding_Util.mkAssume - uu___20 in - let uu___20 = - let uu___21 = - FStar_Compiler_Util.first_N + FStar_SMTEncoding_Util.mkAssume + uu___20 in + let uu___20 = + let uu___21 + = + FStar_Compiler_Util.first_N n_tps formals in - match uu___21 - with - | (uu___22, - formals') + match uu___21 + with + | (uu___22, + formals') -> let uu___23 = @@ -6076,41 +5384,41 @@ and (encode_sigelt' : [uu___28] in (uu___27, cod_decls)))) in - (match uu___20 - with - | (codomain_ordering, - codomain_decls) - -> - ((FStar_Compiler_List.op_At + (match uu___20 + with + | (codomain_ordering, + codomain_decls) + -> + ((FStar_Compiler_List.op_At arg_decls codomain_decls), (FStar_Compiler_List.op_At [typing_inversion; subterm_ordering] codomain_ordering))))) - | FStar_Syntax_Syntax.Tm_fvar - fv -> - let encoded_head_fvb = - FStar_SMTEncoding_Env.lookup_free_var_name - env' - fv.FStar_Syntax_Syntax.fv_name in - let uu___12 = - FStar_SMTEncoding_EncodeTerm.encode_args - args env' in - (match uu___12 with - | (encoded_args, - arg_decls) -> - let guards_for_parameter - orig_arg arg xv = - let fv1 = - match arg.FStar_SMTEncoding_Term.tm - with - | FStar_SMTEncoding_Term.FreeV - fv2 -> fv2 - | uu___13 -> - let uu___14 - = - let uu___15 + | FStar_Syntax_Syntax.Tm_fvar + fv -> + let encoded_head_fvb = + FStar_SMTEncoding_Env.lookup_free_var_name + env' + fv.FStar_Syntax_Syntax.fv_name in + let uu___12 = + FStar_SMTEncoding_EncodeTerm.encode_args + args env' in + (match uu___12 with + | (encoded_args, + arg_decls) -> + let guards_for_parameter + orig_arg arg xv = + let fv1 = + match arg.FStar_SMTEncoding_Term.tm + with + | FStar_SMTEncoding_Term.FreeV + fv2 -> fv2 + | uu___13 -> + let uu___14 + = + let uu___15 = let uu___16 = @@ -6119,15 +5427,15 @@ and (encode_sigelt' : FStar_Compiler_Util.format1 "Inductive type parameter %s must be a variable ; You may want to change it to an index." uu___16 in - (FStar_Errors_Codes.Fatal_NonVariableInductiveTypeParameter, + (FStar_Errors_Codes.Fatal_NonVariableInductiveTypeParameter, uu___15) in - FStar_Errors.raise_error - uu___14 - orig_arg.FStar_Syntax_Syntax.pos in - let guards1 = - FStar_Compiler_List.collect - (fun g -> - let uu___13 + FStar_Errors.raise_error + uu___14 + orig_arg.FStar_Syntax_Syntax.pos in + let guards1 = + FStar_Compiler_List.collect + (fun g -> + let uu___13 = let uu___14 = @@ -6136,31 +5444,32 @@ and (encode_sigelt' : FStar_Compiler_List.contains fv1 uu___14 in - if uu___13 - then + if uu___13 + then let uu___14 = FStar_SMTEncoding_Term.subst g fv1 xv in [uu___14] - else []) - guards in - FStar_SMTEncoding_Util.mk_and_l - guards1 in - let uu___13 = - let uu___14 = - FStar_Compiler_List.zip - args - encoded_args in - FStar_Compiler_List.fold_left - (fun uu___15 -> - fun uu___16 - -> - match + else []) + guards in + FStar_SMTEncoding_Util.mk_and_l + guards1 in + let uu___13 = + let uu___14 = + FStar_Compiler_List.zip + args + encoded_args in + FStar_Compiler_List.fold_left + (fun uu___15 -> + fun uu___16 + -> + match (uu___15, uu___16) - with - | ((env2, + with + | + ((env2, arg_vars, eqns_or_guards, i), @@ -6210,44 +5519,46 @@ and (encode_sigelt' : eqns, (i + Prims.int_one)))) - (env', [], [], - Prims.int_zero) - uu___14 in - (match uu___13 with - | (uu___14, - arg_vars, - elim_eqns_or_guards, - uu___15) -> - let arg_vars1 = - FStar_Compiler_List.rev - arg_vars in - let ty = - FStar_SMTEncoding_EncodeTerm.maybe_curry_fvb - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.p - encoded_head_fvb - arg_vars1 in - let xvars1 = - FStar_Compiler_List.map - FStar_SMTEncoding_Util.mkFreeV - vars in - let dapp1 = - FStar_SMTEncoding_Util.mkApp - (ddconstrsym, + (env', [], [], + Prims.int_zero) + uu___14 in + (match uu___13 with + | (uu___14, + arg_vars, + elim_eqns_or_guards, + uu___15) -> + let arg_vars1 + = + FStar_Compiler_List.rev + arg_vars in + let ty = + FStar_SMTEncoding_EncodeTerm.maybe_curry_fvb + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.p + encoded_head_fvb + arg_vars1 in + let xvars1 = + FStar_Compiler_List.map + FStar_SMTEncoding_Util.mkFreeV + vars in + let dapp1 = + FStar_SMTEncoding_Util.mkApp + (ddconstrsym, xvars1) in - let ty_pred = - FStar_SMTEncoding_Term.mk_HasTypeWithFuel - (FStar_Pervasives_Native.Some + let ty_pred = + FStar_SMTEncoding_Term.mk_HasTypeWithFuel + (FStar_Pervasives_Native.Some s_fuel_tm) - dapp1 ty in - let arg_binders - = - FStar_Compiler_List.map - FStar_SMTEncoding_Term.fv_of_term - arg_vars1 in - let typing_inversion - = - let uu___16 = - let uu___17 + dapp1 ty in + let arg_binders + = + FStar_Compiler_List.map + FStar_SMTEncoding_Term.fv_of_term + arg_vars1 in + let typing_inversion + = + let uu___16 + = + let uu___17 = let uu___18 = @@ -6288,19 +5599,18 @@ and (encode_sigelt' : FStar_SMTEncoding_Term.mkForall uu___18 uu___19 in - (uu___17, - ( - FStar_Pervasives_Native.Some + (uu___17, + (FStar_Pervasives_Native.Some "data constructor typing elim"), - ( - Prims.strcat + (Prims.strcat "data_elim_" ddconstrsym)) in - FStar_SMTEncoding_Util.mkAssume - uu___16 in - let lex_t = - let uu___16 = - let uu___17 + FStar_SMTEncoding_Util.mkAssume + uu___16 in + let lex_t = + let uu___16 + = + let uu___17 = let uu___18 = @@ -6308,14 +5618,14 @@ and (encode_sigelt' : FStar_Parser_Const.lex_t_lid in (uu___18, FStar_SMTEncoding_Term.Term_sort) in - FStar_SMTEncoding_Term.mk_fv + FStar_SMTEncoding_Term.mk_fv uu___17 in - FStar_SMTEncoding_Util.mkFreeV - uu___16 in - let subterm_ordering - = - let prec = - let uu___16 + FStar_SMTEncoding_Util.mkFreeV + uu___16 in + let subterm_ordering + = + let prec = + let uu___16 = FStar_Compiler_List.mapi (fun i -> @@ -6337,10 +5647,11 @@ and (encode_sigelt' : dapp1 in [uu___18])) vars in - FStar_Compiler_List.flatten + FStar_Compiler_List.flatten uu___16 in - let uu___16 = - let uu___17 + let uu___16 + = + let uu___17 = let uu___18 = @@ -6379,25 +5690,24 @@ and (encode_sigelt' : FStar_SMTEncoding_Term.mkForall uu___18 uu___19 in - (uu___17, - ( - FStar_Pervasives_Native.Some + (uu___17, + (FStar_Pervasives_Native.Some "subterm ordering"), - ( - Prims.strcat + (Prims.strcat "subterm_ordering_" ddconstrsym)) in - FStar_SMTEncoding_Util.mkAssume - uu___16 in - let uu___16 = - let uu___17 = - FStar_Compiler_Util.first_N + FStar_SMTEncoding_Util.mkAssume + uu___16 in + let uu___16 = + let uu___17 + = + FStar_Compiler_Util.first_N n_tps formals in - match uu___17 - with - | (uu___18, - formals') + match uu___17 + with + | (uu___18, + formals') -> let uu___19 = @@ -6828,71 +6138,72 @@ and (encode_sigelt' : [uu___24] in (uu___23, cod_decls)))) in - (match uu___16 - with - | (codomain_ordering, - codomain_decls) - -> - ((FStar_Compiler_List.op_At + (match uu___16 + with + | (codomain_ordering, + codomain_decls) + -> + ((FStar_Compiler_List.op_At arg_decls codomain_decls), (FStar_Compiler_List.op_At [typing_inversion; subterm_ordering] codomain_ordering))))) - | uu___12 -> - ((let uu___14 = - let uu___15 = - let uu___16 = - FStar_Syntax_Print.lid_to_string - d in - let uu___17 = - FStar_Syntax_Print.term_to_string - head in - FStar_Compiler_Util.format2 - "Constructor %s builds an unexpected type %s\n" - uu___16 uu___17 in - (FStar_Errors_Codes.Warning_ConstructorBuildsUnexpectedType, - uu___15) in - FStar_Errors.log_issue - se.FStar_Syntax_Syntax.sigrng - uu___14); - ([], []))) in - let uu___9 = encode_elim () in - (match uu___9 with - | (decls2, elim) -> - let data_cons_typing_intro_decl - = - let uu___10 = - match t_res_tm.FStar_SMTEncoding_Term.tm - with - | FStar_SMTEncoding_Term.App - (op, args) -> - let uu___11 = - FStar_Compiler_List.splitAt - n_tps args in - (match uu___11 with - | (targs, iargs) -> - let uu___12 = - let uu___13 = - FStar_Compiler_List.map - (fun uu___14 + | uu___12 -> + ((let uu___14 = + let uu___15 = + let uu___16 = + FStar_Syntax_Print.lid_to_string + d in + let uu___17 = + FStar_Syntax_Print.term_to_string + head in + FStar_Compiler_Util.format2 + "Constructor %s builds an unexpected type %s\n" + uu___16 uu___17 in + (FStar_Errors_Codes.Warning_ConstructorBuildsUnexpectedType, + uu___15) in + FStar_Errors.log_issue + se.FStar_Syntax_Syntax.sigrng + uu___14); + ([], []))) in + let uu___9 = encode_elim () in + (match uu___9 with + | (decls2, elim) -> + let data_cons_typing_intro_decl + = + let uu___10 = + match t_res_tm.FStar_SMTEncoding_Term.tm + with + | FStar_SMTEncoding_Term.App + (op, args) -> + let uu___11 = + FStar_Compiler_List.splitAt + n_tps args in + (match uu___11 with + | (targs, iargs) -> + let uu___12 = + let uu___13 = + FStar_Compiler_List.map + (fun + uu___14 -> FStar_SMTEncoding_Env.fresh_fvar env1.FStar_SMTEncoding_Env.current_module_name "i" FStar_SMTEncoding_Term.Term_sort) - iargs in - FStar_Compiler_List.split - uu___13 in - (match uu___12 - with - | (fresh_ivars, - fresh_iargs) - -> - let additional_guards - = - let uu___13 + iargs in + FStar_Compiler_List.split + uu___13 in + (match uu___12 + with + | (fresh_ivars, + fresh_iargs) + -> + let additional_guards + = + let uu___13 = FStar_Compiler_List.map2 (fun a -> @@ -6904,12 +6215,12 @@ and (encode_sigelt' : fresh_a)) iargs fresh_iargs in - FStar_SMTEncoding_Util.mk_and_l + FStar_SMTEncoding_Util.mk_and_l uu___13 in - let uu___13 = - FStar_SMTEncoding_Term.mk_HasTypeWithFuel - ( - FStar_Pervasives_Native.Some + let uu___13 + = + FStar_SMTEncoding_Term.mk_HasTypeWithFuel + (FStar_Pervasives_Native.Some fuel_tm) dapp { @@ -6927,8 +6238,9 @@ and (encode_sigelt' : = (t_res_tm.FStar_SMTEncoding_Term.rng) } in - let uu___14 = - let uu___15 + let uu___14 + = + let uu___15 = FStar_Compiler_List.map (fun s -> @@ -6936,61 +6248,65 @@ and (encode_sigelt' : (s, FStar_SMTEncoding_Term.Term_sort)) fresh_ivars in - FStar_Compiler_List.op_At + FStar_Compiler_List.op_At vars uu___15 in - let uu___15 = - FStar_SMTEncoding_Util.mkAnd + let uu___15 + = + FStar_SMTEncoding_Util.mkAnd (guard, additional_guards) in - (uu___13, - uu___14, - uu___15))) - | uu___11 -> - (ty_pred', vars, guard) in - match uu___10 with - | (ty_pred'1, vars1, guard1) - -> - let uu___11 = - let uu___12 = - let uu___13 = - FStar_Ident.range_of_lid - d in - let uu___14 = - let uu___15 = - let uu___16 = - FStar_SMTEncoding_Term.mk_fv - (fuel_var, - FStar_SMTEncoding_Term.Fuel_sort) in - FStar_SMTEncoding_Env.add_fuel - uu___16 vars1 in - let uu___16 = - FStar_SMTEncoding_Util.mkImp - (guard1, - ty_pred'1) in - ([[ty_pred'1]], - uu___15, uu___16) in - FStar_SMTEncoding_Term.mkForall - uu___13 uu___14 in - (uu___12, - (FStar_Pervasives_Native.Some - "data constructor typing intro"), - (Prims.strcat - "data_typing_intro_" - ddtok)) in - FStar_SMTEncoding_Util.mkAssume - uu___11 in - let g = - let uu___10 = - let uu___11 = - let uu___12 = - let uu___13 = - let uu___14 = - let uu___15 = - let uu___16 = - let uu___17 = - let uu___18 = - let uu___19 + (uu___13, + uu___14, + uu___15))) + | uu___11 -> + (ty_pred', vars, + guard) in + match uu___10 with + | (ty_pred'1, vars1, guard1) + -> + let uu___11 = + let uu___12 = + let uu___13 = + FStar_Ident.range_of_lid + d in + let uu___14 = + let uu___15 = + let uu___16 = + FStar_SMTEncoding_Term.mk_fv + (fuel_var, + FStar_SMTEncoding_Term.Fuel_sort) in + FStar_SMTEncoding_Env.add_fuel + uu___16 vars1 in + let uu___16 = + FStar_SMTEncoding_Util.mkImp + (guard1, + ty_pred'1) in + ([[ty_pred'1]], + uu___15, + uu___16) in + FStar_SMTEncoding_Term.mkForall + uu___13 uu___14 in + (uu___12, + (FStar_Pervasives_Native.Some + "data constructor typing intro"), + (Prims.strcat + "data_typing_intro_" + ddtok)) in + FStar_SMTEncoding_Util.mkAssume + uu___11 in + let g = + let uu___10 = + let uu___11 = + let uu___12 = + let uu___13 = + let uu___14 = + let uu___15 = + let uu___16 = + let uu___17 = + let uu___18 + = + let uu___19 = let uu___20 = @@ -6999,36 +6315,35 @@ and (encode_sigelt' : FStar_Compiler_Util.format1 "data constructor proxy: %s" uu___20 in - FStar_Pervasives_Native.Some + FStar_Pervasives_Native.Some uu___19 in - (ddtok, [], - FStar_SMTEncoding_Term.Term_sort, - uu___18) in - FStar_SMTEncoding_Term.DeclFun - uu___17 in - [uu___16] in - FStar_Compiler_List.op_At - uu___15 - proxy_fresh in - FStar_SMTEncoding_Term.mk_decls_trivial - uu___14 in - let uu___14 = - let uu___15 = - let uu___16 = - let uu___17 = - let uu___18 = - FStar_SMTEncoding_Util.mkAssume - (tok_typing1, - ( - FStar_Pervasives_Native.Some + (ddtok, [], + FStar_SMTEncoding_Term.Term_sort, + uu___18) in + FStar_SMTEncoding_Term.DeclFun + uu___17 in + [uu___16] in + FStar_Compiler_List.op_At + uu___15 + proxy_fresh in + FStar_SMTEncoding_Term.mk_decls_trivial + uu___14 in + let uu___14 = + let uu___15 = + let uu___16 = + let uu___17 = + let uu___18 = + FStar_SMTEncoding_Util.mkAssume + (tok_typing1, + (FStar_Pervasives_Native.Some "typing for data constructor proxy"), - ( - Prims.strcat + (Prims.strcat "typing_tok_" ddtok)) in - let uu___19 = - let uu___20 = - let uu___21 + let uu___19 = + let uu___20 + = + let uu___21 = let uu___22 = @@ -7055,49 +6370,797 @@ and (encode_sigelt' : (Prims.strcat "equality_tok_" ddtok)) in - FStar_SMTEncoding_Util.mkAssume + FStar_SMTEncoding_Util.mkAssume uu___21 in - [uu___20; - data_cons_typing_intro_decl] in - uu___18 :: - uu___19 in - FStar_Compiler_List.op_At - uu___17 elim in - FStar_SMTEncoding_Term.mk_decls_trivial - uu___16 in - FStar_Compiler_List.op_At - decls_pred uu___15 in - FStar_Compiler_List.op_At - uu___13 uu___14 in - FStar_Compiler_List.op_At - decls3 uu___12 in - FStar_Compiler_List.op_At - decls2 uu___11 in - FStar_Compiler_List.op_At - binder_decls uu___10 in - let uu___10 = - let uu___11 = - FStar_SMTEncoding_Term.mk_decls_trivial - datacons in - FStar_Compiler_List.op_At - uu___11 g in - (uu___10, env1))))))))) -and (encode_sigelts : + [uu___20; + data_cons_typing_intro_decl] in + uu___18 :: + uu___19 in + FStar_Compiler_List.op_At + uu___17 elim in + FStar_SMTEncoding_Term.mk_decls_trivial + uu___16 in + FStar_Compiler_List.op_At + decls_pred uu___15 in + FStar_Compiler_List.op_At + uu___13 uu___14 in + FStar_Compiler_List.op_At + decls3 uu___12 in + FStar_Compiler_List.op_At + decls2 uu___11 in + FStar_Compiler_List.op_At + binder_decls uu___10 in + let uu___10 = + let uu___11 = + FStar_SMTEncoding_Term.mk_decls_trivial + datacons in + FStar_Compiler_List.op_At + uu___11 g in + (uu___10, env1)))))))) +let rec (encode_sigelt : FStar_SMTEncoding_Env.env_t -> - FStar_Syntax_Syntax.sigelt Prims.list -> + FStar_Syntax_Syntax.sigelt -> (FStar_SMTEncoding_Term.decls_t * FStar_SMTEncoding_Env.env_t)) = fun env -> - fun ses -> - FStar_Compiler_List.fold_left - (fun uu___ -> - fun se -> - match uu___ with - | (g, env1) -> - let uu___1 = encode_sigelt env1 se in - (match uu___1 with - | (g', env2) -> ((FStar_Compiler_List.op_At g g'), env2))) - ([], env) ses + fun se -> + let nm = FStar_Syntax_Print.sigelt_to_string_short se in + let uu___ = + let uu___1 = + let uu___2 = FStar_Syntax_Print.sigelt_to_string_short se in + FStar_Compiler_Util.format1 + "While encoding top-level declaration `%s`" uu___2 in + FStar_Errors.with_ctx uu___1 (fun uu___2 -> encode_sigelt' env se) in + match uu___ with + | (g, env1) -> + let g1 = + match g with + | [] -> + ((let uu___2 = + FStar_TypeChecker_Env.debug + env1.FStar_SMTEncoding_Env.tcenv + (FStar_Options.Other "SMTEncoding") in + if uu___2 + then + FStar_Compiler_Util.print1 "Skipped encoding of %s\n" nm + else ()); + (let uu___2 = + let uu___3 = + let uu___4 = + FStar_Compiler_Util.format1 "" nm in + FStar_SMTEncoding_Term.Caption uu___4 in + [uu___3] in + FStar_SMTEncoding_Term.mk_decls_trivial uu___2)) + | uu___1 -> + let uu___2 = + let uu___3 = + let uu___4 = + let uu___5 = + FStar_Compiler_Util.format1 "" nm in + FStar_SMTEncoding_Term.Caption uu___5 in + [uu___4] in + FStar_SMTEncoding_Term.mk_decls_trivial uu___3 in + let uu___3 = + let uu___4 = + let uu___5 = + let uu___6 = + let uu___7 = + FStar_Compiler_Util.format1 "" nm in + FStar_SMTEncoding_Term.Caption uu___7 in + [uu___6] in + FStar_SMTEncoding_Term.mk_decls_trivial uu___5 in + FStar_Compiler_List.op_At g uu___4 in + FStar_Compiler_List.op_At uu___2 uu___3 in + (g1, env1) +and (encode_sigelt' : + FStar_SMTEncoding_Env.env_t -> + FStar_Syntax_Syntax.sigelt -> + (FStar_SMTEncoding_Term.decls_t * FStar_SMTEncoding_Env.env_t)) + = + fun env -> + fun se -> + (let uu___1 = + FStar_TypeChecker_Env.debug env.FStar_SMTEncoding_Env.tcenv + (FStar_Options.Other "SMTEncoding") in + if uu___1 + then + let uu___2 = FStar_Syntax_Print.sigelt_to_string se in + FStar_Compiler_Util.print1 "@@@Encoding sigelt %s\n" uu___2 + else ()); + (let is_opaque_to_smt t = + let uu___1 = + let uu___2 = FStar_Syntax_Subst.compress t in + uu___2.FStar_Syntax_Syntax.n in + match uu___1 with + | FStar_Syntax_Syntax.Tm_constant (FStar_Const.Const_string + (s, uu___2)) -> s = "opaque_to_smt" + | uu___2 -> false in + let is_uninterpreted_by_smt t = + let uu___1 = + let uu___2 = FStar_Syntax_Subst.compress t in + uu___2.FStar_Syntax_Syntax.n in + match uu___1 with + | FStar_Syntax_Syntax.Tm_constant (FStar_Const.Const_string + (s, uu___2)) -> s = "uninterpreted_by_smt" + | uu___2 -> false in + match se.FStar_Syntax_Syntax.sigel with + | FStar_Syntax_Syntax.Sig_splice uu___1 -> + FStar_Compiler_Effect.failwith + "impossible -- splice should have been removed by Tc.fs" + | FStar_Syntax_Syntax.Sig_fail uu___1 -> + FStar_Compiler_Effect.failwith + "impossible -- Sig_fail should have been removed by Tc.fs" + | FStar_Syntax_Syntax.Sig_pragma uu___1 -> ([], env) + | FStar_Syntax_Syntax.Sig_effect_abbrev uu___1 -> ([], env) + | FStar_Syntax_Syntax.Sig_sub_effect uu___1 -> ([], env) + | FStar_Syntax_Syntax.Sig_polymonadic_bind uu___1 -> ([], env) + | FStar_Syntax_Syntax.Sig_polymonadic_subcomp uu___1 -> ([], env) + | FStar_Syntax_Syntax.Sig_new_effect ed -> + let uu___1 = + let uu___2 = + FStar_SMTEncoding_Util.is_smt_reifiable_effect + env.FStar_SMTEncoding_Env.tcenv ed.FStar_Syntax_Syntax.mname in + Prims.op_Negation uu___2 in + if uu___1 + then ([], env) + else + (let close_effect_params tm = + match ed.FStar_Syntax_Syntax.binders with + | [] -> tm + | uu___3 -> + FStar_Syntax_Syntax.mk + (FStar_Syntax_Syntax.Tm_abs + { + FStar_Syntax_Syntax.bs = + (ed.FStar_Syntax_Syntax.binders); + FStar_Syntax_Syntax.body = tm; + FStar_Syntax_Syntax.rc_opt = + (FStar_Pervasives_Native.Some + (FStar_Syntax_Util.mk_residual_comp + FStar_Parser_Const.effect_Tot_lid + FStar_Pervasives_Native.None + [FStar_Syntax_Syntax.TOTAL])) + }) tm.FStar_Syntax_Syntax.pos in + let encode_action env1 a = + let action_defn = + let uu___3 = + close_effect_params a.FStar_Syntax_Syntax.action_defn in + norm_before_encoding env1 uu___3 in + let uu___3 = + FStar_Syntax_Util.arrow_formals_comp + a.FStar_Syntax_Syntax.action_typ in + match uu___3 with + | (formals, uu___4) -> + let arity = FStar_Compiler_List.length formals in + let uu___5 = + FStar_SMTEncoding_Env.new_term_constant_and_tok_from_lid + env1 a.FStar_Syntax_Syntax.action_name arity in + (match uu___5 with + | (aname, atok, env2) -> + let uu___6 = + FStar_SMTEncoding_EncodeTerm.encode_term + action_defn env2 in + (match uu___6 with + | (tm, decls) -> + let a_decls = + let uu___7 = + let uu___8 = + let uu___9 = + FStar_Compiler_List.map + (fun uu___10 -> + FStar_SMTEncoding_Term.Term_sort) + formals in + (aname, uu___9, + FStar_SMTEncoding_Term.Term_sort, + (FStar_Pervasives_Native.Some "Action")) in + FStar_SMTEncoding_Term.DeclFun uu___8 in + [uu___7; + FStar_SMTEncoding_Term.DeclFun + (atok, [], + FStar_SMTEncoding_Term.Term_sort, + (FStar_Pervasives_Native.Some + "Action token"))] in + let uu___7 = + let aux uu___8 uu___9 = + match (uu___8, uu___9) with + | ({ FStar_Syntax_Syntax.binder_bv = bv; + FStar_Syntax_Syntax.binder_qual = + uu___10; + FStar_Syntax_Syntax.binder_positivity + = uu___11; + FStar_Syntax_Syntax.binder_attrs = + uu___12;_}, + (env3, acc_sorts, acc)) -> + let uu___13 = + FStar_SMTEncoding_Env.gen_term_var + env3 bv in + (match uu___13 with + | (xxsym, xx, env4) -> + let uu___14 = + let uu___15 = + FStar_SMTEncoding_Term.mk_fv + (xxsym, + FStar_SMTEncoding_Term.Term_sort) in + uu___15 :: acc_sorts in + (env4, uu___14, (xx :: acc))) in + FStar_Compiler_List.fold_right aux formals + (env2, [], []) in + (match uu___7 with + | (uu___8, xs_sorts, xs) -> + let app = + FStar_SMTEncoding_Util.mkApp (aname, xs) in + let a_eq = + let uu___9 = + let uu___10 = + let uu___11 = + FStar_Ident.range_of_lid + a.FStar_Syntax_Syntax.action_name in + let uu___12 = + let uu___13 = + let uu___14 = + let uu___15 = + FStar_SMTEncoding_EncodeTerm.mk_Apply + tm xs_sorts in + (app, uu___15) in + FStar_SMTEncoding_Util.mkEq + uu___14 in + ([[app]], xs_sorts, uu___13) in + FStar_SMTEncoding_Term.mkForall + uu___11 uu___12 in + (uu___10, + (FStar_Pervasives_Native.Some + "Action equality"), + (Prims.strcat aname "_equality")) in + FStar_SMTEncoding_Util.mkAssume uu___9 in + let tok_correspondence = + let tok_term = + let uu___9 = + FStar_SMTEncoding_Term.mk_fv + (atok, + FStar_SMTEncoding_Term.Term_sort) in + FStar_SMTEncoding_Util.mkFreeV uu___9 in + let tok_app = + FStar_SMTEncoding_EncodeTerm.mk_Apply + tok_term xs_sorts in + let uu___9 = + let uu___10 = + let uu___11 = + FStar_Ident.range_of_lid + a.FStar_Syntax_Syntax.action_name in + let uu___12 = + let uu___13 = + FStar_SMTEncoding_Util.mkEq + (tok_app, app) in + ([[tok_app]], xs_sorts, uu___13) in + FStar_SMTEncoding_Term.mkForall + uu___11 uu___12 in + (uu___10, + (FStar_Pervasives_Native.Some + "Action token correspondence"), + (Prims.strcat aname + "_token_correspondence")) in + FStar_SMTEncoding_Util.mkAssume uu___9 in + let uu___9 = + let uu___10 = + FStar_SMTEncoding_Term.mk_decls_trivial + (FStar_Compiler_List.op_At a_decls + [a_eq; tok_correspondence]) in + FStar_Compiler_List.op_At decls uu___10 in + (env2, uu___9)))) in + let uu___3 = + FStar_Compiler_Util.fold_map encode_action env + ed.FStar_Syntax_Syntax.actions in + match uu___3 with + | (env1, decls2) -> + ((FStar_Compiler_List.flatten decls2), env1)) + | FStar_Syntax_Syntax.Sig_declare_typ + { FStar_Syntax_Syntax.lid2 = lid; + FStar_Syntax_Syntax.us2 = uu___1; + FStar_Syntax_Syntax.t2 = uu___2;_} + when FStar_Ident.lid_equals lid FStar_Parser_Const.precedes_lid -> + let uu___3 = + FStar_SMTEncoding_Env.new_term_constant_and_tok_from_lid env lid + (Prims.of_int (4)) in + (match uu___3 with | (tname, ttok, env1) -> ([], env1)) + | FStar_Syntax_Syntax.Sig_declare_typ + { FStar_Syntax_Syntax.lid2 = lid; + FStar_Syntax_Syntax.us2 = uu___1; FStar_Syntax_Syntax.t2 = t;_} + -> + let quals = se.FStar_Syntax_Syntax.sigquals in + let will_encode_definition = + let uu___2 = + FStar_Compiler_Util.for_some + (fun uu___3 -> + match uu___3 with + | FStar_Syntax_Syntax.Assumption -> true + | FStar_Syntax_Syntax.Projector uu___4 -> true + | FStar_Syntax_Syntax.Discriminator uu___4 -> true + | FStar_Syntax_Syntax.Irreducible -> true + | uu___4 -> false) quals in + Prims.op_Negation uu___2 in + if will_encode_definition + then ([], env) + else + (let fv = + FStar_Syntax_Syntax.lid_as_fv lid + FStar_Pervasives_Native.None in + let uu___3 = + let uu___4 = + FStar_Compiler_Util.for_some is_uninterpreted_by_smt + se.FStar_Syntax_Syntax.sigattrs in + encode_top_level_val uu___4 env fv t quals in + match uu___3 with + | (decls, env1) -> + let tname = FStar_Ident.string_of_lid lid in + let tsym = + let uu___4 = + FStar_SMTEncoding_Env.try_lookup_free_var env1 lid in + FStar_Compiler_Option.get uu___4 in + let uu___4 = + let uu___5 = + let uu___6 = + primitive_type_axioms + env1.FStar_SMTEncoding_Env.tcenv lid tname tsym in + FStar_SMTEncoding_Term.mk_decls_trivial uu___6 in + FStar_Compiler_List.op_At decls uu___5 in + (uu___4, env1)) + | FStar_Syntax_Syntax.Sig_assume + { FStar_Syntax_Syntax.lid3 = l; FStar_Syntax_Syntax.us3 = us; + FStar_Syntax_Syntax.phi1 = f;_} + -> + let uu___1 = FStar_Syntax_Subst.open_univ_vars us f in + (match uu___1 with + | (uvs, f1) -> + let env1 = + let uu___2 = + FStar_TypeChecker_Env.push_univ_vars + env.FStar_SMTEncoding_Env.tcenv uvs in + { + FStar_SMTEncoding_Env.bvar_bindings = + (env.FStar_SMTEncoding_Env.bvar_bindings); + FStar_SMTEncoding_Env.fvar_bindings = + (env.FStar_SMTEncoding_Env.fvar_bindings); + FStar_SMTEncoding_Env.depth = + (env.FStar_SMTEncoding_Env.depth); + FStar_SMTEncoding_Env.tcenv = uu___2; + FStar_SMTEncoding_Env.warn = + (env.FStar_SMTEncoding_Env.warn); + FStar_SMTEncoding_Env.nolabels = + (env.FStar_SMTEncoding_Env.nolabels); + FStar_SMTEncoding_Env.use_zfuel_name = + (env.FStar_SMTEncoding_Env.use_zfuel_name); + FStar_SMTEncoding_Env.encode_non_total_function_typ = + (env.FStar_SMTEncoding_Env.encode_non_total_function_typ); + FStar_SMTEncoding_Env.current_module_name = + (env.FStar_SMTEncoding_Env.current_module_name); + FStar_SMTEncoding_Env.encoding_quantifier = + (env.FStar_SMTEncoding_Env.encoding_quantifier); + FStar_SMTEncoding_Env.global_cache = + (env.FStar_SMTEncoding_Env.global_cache) + } in + let f2 = norm_before_encoding env1 f1 in + let uu___2 = + FStar_SMTEncoding_EncodeTerm.encode_formula f2 env1 in + (match uu___2 with + | (f3, decls) -> + let g = + let uu___3 = + let uu___4 = + let uu___5 = + let uu___6 = + let uu___7 = + let uu___8 = + FStar_Syntax_Print.lid_to_string l in + FStar_Compiler_Util.format1 "Assumption: %s" + uu___8 in + FStar_Pervasives_Native.Some uu___7 in + let uu___7 = + let uu___8 = + let uu___9 = FStar_Ident.string_of_lid l in + Prims.strcat "assumption_" uu___9 in + FStar_SMTEncoding_Env.varops.FStar_SMTEncoding_Env.mk_unique + uu___8 in + (f3, uu___6, uu___7) in + FStar_SMTEncoding_Util.mkAssume uu___5 in + [uu___4] in + FStar_SMTEncoding_Term.mk_decls_trivial uu___3 in + ((FStar_Compiler_List.op_At decls g), env1))) + | FStar_Syntax_Syntax.Sig_let + { FStar_Syntax_Syntax.lbs1 = lbs; + FStar_Syntax_Syntax.lids1 = uu___1;_} + when + (FStar_Compiler_List.contains FStar_Syntax_Syntax.Irreducible + se.FStar_Syntax_Syntax.sigquals) + || + (FStar_Compiler_Util.for_some is_opaque_to_smt + se.FStar_Syntax_Syntax.sigattrs) + -> + let attrs = se.FStar_Syntax_Syntax.sigattrs in + let uu___2 = + FStar_Compiler_Util.fold_map + (fun env1 -> + fun lb -> + let lid = + let uu___3 = + let uu___4 = + FStar_Compiler_Util.right + lb.FStar_Syntax_Syntax.lbname in + uu___4.FStar_Syntax_Syntax.fv_name in + uu___3.FStar_Syntax_Syntax.v in + let uu___3 = + let uu___4 = + FStar_TypeChecker_Env.try_lookup_val_decl + env1.FStar_SMTEncoding_Env.tcenv lid in + FStar_Compiler_Option.isNone uu___4 in + if uu___3 + then + let val_decl = + { + FStar_Syntax_Syntax.sigel = + (FStar_Syntax_Syntax.Sig_declare_typ + { + FStar_Syntax_Syntax.lid2 = lid; + FStar_Syntax_Syntax.us2 = + (lb.FStar_Syntax_Syntax.lbunivs); + FStar_Syntax_Syntax.t2 = + (lb.FStar_Syntax_Syntax.lbtyp) + }); + FStar_Syntax_Syntax.sigrng = + (se.FStar_Syntax_Syntax.sigrng); + FStar_Syntax_Syntax.sigquals = + (FStar_Syntax_Syntax.Irreducible :: + (se.FStar_Syntax_Syntax.sigquals)); + FStar_Syntax_Syntax.sigmeta = + (se.FStar_Syntax_Syntax.sigmeta); + FStar_Syntax_Syntax.sigattrs = + (se.FStar_Syntax_Syntax.sigattrs); + FStar_Syntax_Syntax.sigopens_and_abbrevs = + (se.FStar_Syntax_Syntax.sigopens_and_abbrevs); + FStar_Syntax_Syntax.sigopts = + (se.FStar_Syntax_Syntax.sigopts) + } in + let uu___4 = encode_sigelt' env1 val_decl in + match uu___4 with | (decls, env2) -> (env2, decls) + else (env1, [])) env (FStar_Pervasives_Native.snd lbs) in + (match uu___2 with + | (env1, decls) -> ((FStar_Compiler_List.flatten decls), env1)) + | FStar_Syntax_Syntax.Sig_let + { + FStar_Syntax_Syntax.lbs1 = + (uu___1, + { FStar_Syntax_Syntax.lbname = FStar_Pervasives.Inr b2t; + FStar_Syntax_Syntax.lbunivs = uu___2; + FStar_Syntax_Syntax.lbtyp = uu___3; + FStar_Syntax_Syntax.lbeff = uu___4; + FStar_Syntax_Syntax.lbdef = uu___5; + FStar_Syntax_Syntax.lbattrs = uu___6; + FStar_Syntax_Syntax.lbpos = uu___7;_}::[]); + FStar_Syntax_Syntax.lids1 = uu___8;_} + when FStar_Syntax_Syntax.fv_eq_lid b2t FStar_Parser_Const.b2t_lid + -> + let uu___9 = + FStar_SMTEncoding_Env.new_term_constant_and_tok_from_lid env + (b2t.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v + Prims.int_one in + (match uu___9 with + | (tname, ttok, env1) -> + let xx = + FStar_SMTEncoding_Term.mk_fv + ("x", FStar_SMTEncoding_Term.Term_sort) in + let x = FStar_SMTEncoding_Util.mkFreeV xx in + let b2t_x = FStar_SMTEncoding_Util.mkApp ("Prims.b2t", [x]) in + let valid_b2t_x = + FStar_SMTEncoding_Util.mkApp ("Valid", [b2t_x]) in + let bool_ty = + let uu___10 = + FStar_Syntax_Syntax.withsort FStar_Parser_Const.bool_lid in + FStar_SMTEncoding_Env.lookup_free_var env1 uu___10 in + let decls = + let uu___10 = + let uu___11 = + let uu___12 = + let uu___13 = + let uu___14 = FStar_Syntax_Syntax.range_of_fv b2t in + let uu___15 = + let uu___16 = + let uu___17 = + let uu___18 = + FStar_SMTEncoding_Util.mkApp + ((FStar_Pervasives_Native.snd + FStar_SMTEncoding_Term.boxBoolFun), + [x]) in + (valid_b2t_x, uu___18) in + FStar_SMTEncoding_Util.mkEq uu___17 in + ([[b2t_x]], [xx], uu___16) in + FStar_SMTEncoding_Term.mkForall uu___14 uu___15 in + (uu___13, (FStar_Pervasives_Native.Some "b2t def"), + "b2t_def") in + FStar_SMTEncoding_Util.mkAssume uu___12 in + let uu___12 = + let uu___13 = + let uu___14 = + let uu___15 = + let uu___16 = FStar_Syntax_Syntax.range_of_fv b2t in + let uu___17 = + let uu___18 = + let uu___19 = + let uu___20 = + FStar_SMTEncoding_Term.mk_HasType x + bool_ty in + let uu___21 = + FStar_SMTEncoding_Term.mk_HasType b2t_x + FStar_SMTEncoding_Term.mk_Term_type in + (uu___20, uu___21) in + FStar_SMTEncoding_Util.mkImp uu___19 in + ([[b2t_x]], [xx], uu___18) in + FStar_SMTEncoding_Term.mkForall uu___16 uu___17 in + (uu___15, + (FStar_Pervasives_Native.Some "b2t typing"), + "b2t_typing") in + FStar_SMTEncoding_Util.mkAssume uu___14 in + [uu___13] in + uu___11 :: uu___12 in + (FStar_SMTEncoding_Term.DeclFun + (tname, [FStar_SMTEncoding_Term.Term_sort], + FStar_SMTEncoding_Term.Term_sort, + FStar_Pervasives_Native.None)) + :: uu___10 in + let uu___10 = FStar_SMTEncoding_Term.mk_decls_trivial decls in + (uu___10, env1)) + | FStar_Syntax_Syntax.Sig_let uu___1 when + FStar_Compiler_Util.for_some + (fun uu___2 -> + match uu___2 with + | FStar_Syntax_Syntax.Discriminator uu___3 -> true + | uu___3 -> false) se.FStar_Syntax_Syntax.sigquals + -> + ((let uu___3 = + FStar_TypeChecker_Env.debug env.FStar_SMTEncoding_Env.tcenv + (FStar_Options.Other "SMTEncoding") in + if uu___3 + then + let uu___4 = FStar_Syntax_Print.sigelt_to_string_short se in + FStar_Compiler_Util.print1 "Not encoding discriminator '%s'\n" + uu___4 + else ()); + ([], env)) + | FStar_Syntax_Syntax.Sig_let + { FStar_Syntax_Syntax.lbs1 = uu___1; + FStar_Syntax_Syntax.lids1 = lids;_} + when + (FStar_Compiler_Util.for_some + (fun l -> + let uu___2 = + let uu___3 = + let uu___4 = FStar_Ident.ns_of_lid l in + FStar_Compiler_List.hd uu___4 in + FStar_Ident.string_of_id uu___3 in + uu___2 = "Prims") lids) + && + (FStar_Compiler_Util.for_some + (fun uu___2 -> + match uu___2 with + | FStar_Syntax_Syntax.Unfold_for_unification_and_vcgen -> + true + | uu___3 -> false) se.FStar_Syntax_Syntax.sigquals) + -> + ((let uu___3 = + FStar_TypeChecker_Env.debug env.FStar_SMTEncoding_Env.tcenv + (FStar_Options.Other "SMTEncoding") in + if uu___3 + then + let uu___4 = FStar_Syntax_Print.sigelt_to_string_short se in + FStar_Compiler_Util.print1 + "Not encoding unfold let from Prims '%s'\n" uu___4 + else ()); + ([], env)) + | FStar_Syntax_Syntax.Sig_let + { FStar_Syntax_Syntax.lbs1 = (false, lb::[]); + FStar_Syntax_Syntax.lids1 = uu___1;_} + when + FStar_Compiler_Util.for_some + (fun uu___2 -> + match uu___2 with + | FStar_Syntax_Syntax.Projector uu___3 -> true + | uu___3 -> false) se.FStar_Syntax_Syntax.sigquals + -> + let fv = FStar_Compiler_Util.right lb.FStar_Syntax_Syntax.lbname in + let l = (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in + let uu___2 = FStar_SMTEncoding_Env.try_lookup_free_var env l in + (match uu___2 with + | FStar_Pervasives_Native.Some uu___3 -> ([], env) + | FStar_Pervasives_Native.None -> + let se1 = + let uu___3 = FStar_Ident.range_of_lid l in + { + FStar_Syntax_Syntax.sigel = + (FStar_Syntax_Syntax.Sig_declare_typ + { + FStar_Syntax_Syntax.lid2 = l; + FStar_Syntax_Syntax.us2 = + (lb.FStar_Syntax_Syntax.lbunivs); + FStar_Syntax_Syntax.t2 = + (lb.FStar_Syntax_Syntax.lbtyp) + }); + FStar_Syntax_Syntax.sigrng = uu___3; + FStar_Syntax_Syntax.sigquals = + (se.FStar_Syntax_Syntax.sigquals); + FStar_Syntax_Syntax.sigmeta = + (se.FStar_Syntax_Syntax.sigmeta); + FStar_Syntax_Syntax.sigattrs = + (se.FStar_Syntax_Syntax.sigattrs); + FStar_Syntax_Syntax.sigopens_and_abbrevs = + (se.FStar_Syntax_Syntax.sigopens_and_abbrevs); + FStar_Syntax_Syntax.sigopts = + (se.FStar_Syntax_Syntax.sigopts) + } in + encode_sigelt env se1) + | FStar_Syntax_Syntax.Sig_let + { FStar_Syntax_Syntax.lbs1 = (is_rec, bindings); + FStar_Syntax_Syntax.lids1 = uu___1;_} + -> + let bindings1 = + FStar_Compiler_List.map + (fun lb -> + let def = + norm_before_encoding env lb.FStar_Syntax_Syntax.lbdef in + let typ = + norm_before_encoding env lb.FStar_Syntax_Syntax.lbtyp in + { + FStar_Syntax_Syntax.lbname = + (lb.FStar_Syntax_Syntax.lbname); + FStar_Syntax_Syntax.lbunivs = + (lb.FStar_Syntax_Syntax.lbunivs); + FStar_Syntax_Syntax.lbtyp = typ; + FStar_Syntax_Syntax.lbeff = + (lb.FStar_Syntax_Syntax.lbeff); + FStar_Syntax_Syntax.lbdef = def; + FStar_Syntax_Syntax.lbattrs = + (lb.FStar_Syntax_Syntax.lbattrs); + FStar_Syntax_Syntax.lbpos = + (lb.FStar_Syntax_Syntax.lbpos) + }) bindings in + encode_top_level_let env (is_rec, bindings1) + se.FStar_Syntax_Syntax.sigquals + | FStar_Syntax_Syntax.Sig_bundle + { FStar_Syntax_Syntax.ses = ses; + FStar_Syntax_Syntax.lids = uu___1;_} + -> + let tycon = + FStar_Compiler_List.tryFind + (fun se1 -> + FStar_Syntax_Syntax.uu___is_Sig_inductive_typ + se1.FStar_Syntax_Syntax.sigel) ses in + let is_injective_on_params = + match tycon with + | FStar_Pervasives_Native.None -> + FStar_Compiler_Effect.failwith + "Impossible: Sig_bundle without a Sig_inductive_typ" + | FStar_Pervasives_Native.Some se1 -> + is_sig_inductive_injective_on_params env se1 in + let uu___2 = + FStar_Compiler_List.fold_left + (fun uu___3 -> + fun se1 -> + match uu___3 with + | (g, env1) -> + let uu___4 = + match se1.FStar_Syntax_Syntax.sigel with + | FStar_Syntax_Syntax.Sig_inductive_typ uu___5 -> + encode_sig_inductive is_injective_on_params + env1 se1 + | FStar_Syntax_Syntax.Sig_datacon uu___5 -> + encode_datacon is_injective_on_params env1 se1 + | uu___5 -> encode_sigelt env1 se1 in + (match uu___4 with + | (g', env2) -> + ((FStar_Compiler_List.op_At g g'), env2))) + ([], env) ses in + (match uu___2 with + | (g, env1) -> + let uu___3 = + FStar_Compiler_List.fold_left + (fun uu___4 -> + fun elt -> + match uu___4 with + | (g', inversions) -> + let uu___5 = + FStar_Compiler_List.partition + (fun uu___6 -> + match uu___6 with + | FStar_SMTEncoding_Term.Assume + { + FStar_SMTEncoding_Term.assumption_term + = uu___7; + FStar_SMTEncoding_Term.assumption_caption + = FStar_Pervasives_Native.Some + "inversion axiom"; + FStar_SMTEncoding_Term.assumption_name + = uu___8; + FStar_SMTEncoding_Term.assumption_fact_ids + = uu___9;_} + -> false + | uu___7 -> true) + elt.FStar_SMTEncoding_Term.decls in + (match uu___5 with + | (elt_g', elt_inversions) -> + ((FStar_Compiler_List.op_At g' + [{ + FStar_SMTEncoding_Term.sym_name = + (elt.FStar_SMTEncoding_Term.sym_name); + FStar_SMTEncoding_Term.key = + (elt.FStar_SMTEncoding_Term.key); + FStar_SMTEncoding_Term.decls = + elt_g'; + FStar_SMTEncoding_Term.a_names = + (elt.FStar_SMTEncoding_Term.a_names) + }]), + (FStar_Compiler_List.op_At inversions + elt_inversions)))) ([], []) g in + (match uu___3 with + | (g', inversions) -> + let uu___4 = + FStar_Compiler_List.fold_left + (fun uu___5 -> + fun elt -> + match uu___5 with + | (decls, elts, rest) -> + let uu___6 = + (FStar_Compiler_Util.is_some + elt.FStar_SMTEncoding_Term.key) + && + (FStar_Compiler_List.existsb + (fun uu___7 -> + match uu___7 with + | FStar_SMTEncoding_Term.DeclFun + uu___8 -> true + | uu___8 -> false) + elt.FStar_SMTEncoding_Term.decls) in + if uu___6 + then + (decls, + (FStar_Compiler_List.op_At elts [elt]), + rest) + else + (let uu___8 = + FStar_Compiler_List.partition + (fun uu___9 -> + match uu___9 with + | FStar_SMTEncoding_Term.DeclFun + uu___10 -> true + | uu___10 -> false) + elt.FStar_SMTEncoding_Term.decls in + match uu___8 with + | (elt_decls, elt_rest) -> + ((FStar_Compiler_List.op_At decls + elt_decls), elts, + (FStar_Compiler_List.op_At rest + [{ + FStar_SMTEncoding_Term.sym_name + = + (elt.FStar_SMTEncoding_Term.sym_name); + FStar_SMTEncoding_Term.key = + (elt.FStar_SMTEncoding_Term.key); + FStar_SMTEncoding_Term.decls + = elt_rest; + FStar_SMTEncoding_Term.a_names + = + (elt.FStar_SMTEncoding_Term.a_names) + }])))) ([], [], []) g' in + (match uu___4 with + | (decls, elts, rest) -> + let uu___5 = + let uu___6 = + FStar_SMTEncoding_Term.mk_decls_trivial decls in + let uu___7 = + let uu___8 = + let uu___9 = + FStar_SMTEncoding_Term.mk_decls_trivial + inversions in + FStar_Compiler_List.op_At rest uu___9 in + FStar_Compiler_List.op_At elts uu___8 in + FStar_Compiler_List.op_At uu___6 uu___7 in + (uu___5, env1))))) let (encode_env_bindings : FStar_SMTEncoding_Env.env_t -> FStar_Syntax_Syntax.binding Prims.list -> diff --git a/src/smtencoding/FStar.SMTEncoding.Encode.fst b/src/smtencoding/FStar.SMTEncoding.Encode.fst index dc6e2598d7e..0f55936367d 100644 --- a/src/smtencoding/FStar.SMTEncoding.Encode.fst +++ b/src/smtencoding/FStar.SMTEncoding.Encode.fst @@ -1000,6 +1000,542 @@ let encode_top_level_let : [decl] |> mk_decls_trivial, env +let is_sig_inductive_injective_on_params (env:env_t) (se:sigelt) + : bool + = let Sig_inductive_typ { lid=t; us=universe_names; params=tps; t=k } = se.sigel in + let t_lid = t in + let tcenv = env.tcenv in + let usubst, uvs = SS.univ_var_opening universe_names in + let tcenv, tps, k = + Env.push_univ_vars tcenv uvs, + SS.subst_binders usubst tps, + SS.subst (SS.shift_subst (List.length tps) usubst) k + in + let tps, k = SS.open_term tps k in + let _, k = U.arrow_formals k in //don't care about indices here + let tps, env_tps, _, us = TcTerm.tc_binders tcenv tps in + let u_k = + TcTerm.level_of_type + env_tps + (S.mk_Tm_app + (S.fvar t None) + (snd (U.args_of_binders tps)) + (Ident.range_of_lid t)) + k + in + //BU.print2 "Universe of tycon: %s : %s\n" (Ident.string_of_lid t) (Print.univ_to_string u_k); + let rec universe_leq u v = + match u, v with + | U_zero, _ -> true + | U_succ u0, U_succ v0 -> universe_leq u0 v0 + | U_name u0, U_name v0 -> Ident.ident_equals u0 v0 + | U_name _, U_succ v0 -> universe_leq u v0 + | U_max us, _ -> us |> BU.for_all (fun u -> universe_leq u v) + | _, U_max vs -> vs |> BU.for_some (universe_leq u) + | U_unknown, _ + | _, U_unknown + | U_unif _, _ + | _, U_unif _ -> failwith (BU.format3 "Impossible: Unresolved or unknown universe in inductive type %s (%s, %s)" + (Ident.string_of_lid t) + (Print.univ_to_string u) + (Print.univ_to_string v)) + | _ -> false + in + let u_leq_u_k u = + let u = N.normalize_universe env_tps u in + universe_leq u u_k + in + let tp_ok (tp:S.binder) (u_tp:universe) = + let t_tp = tp.binder_bv.sort in + if u_leq_u_k u_tp + then true + else ( + let t_tp = + N.normalize + [Unrefine; Unascribe; Unmeta; + Primops; HNF; UnfoldUntil delta_constant; Beta] + env_tps t_tp + in + let formals, t = U.arrow_formals t_tp in + let _, _, _, u_formals = TcTerm.tc_binders env_tps formals in + let inj = BU.for_all (fun u_formal -> u_leq_u_k u_formal) u_formals in + if inj + then ( + match (SS.compress t).n with + | Tm_type u -> + (* retain injectivity for parameters that are type functions + from small universes (i.e., all formals are smaller than the constructed type) + to a universe <= the universe of the constructed type. + See BugBoxInjectivity.fst *) + u_leq_u_k u + | _ -> + false + ) + else ( + false + ) + + ) + in + let is_injective_on_params = List.forall2 tp_ok tps us in + if Env.debug env.tcenv <| Options.Other "SMTEncoding" + then BU.print2 "%s injectivity for %s\n" + (if is_injective_on_params then "YES" else "NO") + (Ident.string_of_lid t); + is_injective_on_params + + +let encode_sig_inductive (is_injective_on_params:bool) (env:env_t) (se:sigelt) +: decls_t * env_t += let Sig_inductive_typ { lid=t; us=universe_names; params=tps; t=k; ds=datas} = se.sigel in + let t_lid = t in + let tcenv = env.tcenv in + let quals = se.sigquals in + let is_logical = quals |> BU.for_some (function Logic | Assumption -> true | _ -> false) in + let constructor_or_logic_type_decl (c:constructor_t) = + if is_logical + then [Term.DeclFun(c.constr_name, c.constr_fields |> List.map (fun f -> f.field_sort), Term_sort, None)] + else constructor_to_decl (Ident.range_of_lid t) c in + let inversion_axioms env tapp vars = + if datas |> BU.for_some (fun l -> Env.try_lookup_lid env.tcenv l |> Option.isNone) //Q: Why would this happen? + then [] + else ( + let xxsym, xx = fresh_fvar env.current_module_name "x" Term_sort in + let data_ax, decls = + datas |> + List.fold_left + (fun (out, decls) l -> + let _, data_t = Env.lookup_datacon env.tcenv l in + let args, res = U.arrow_formals data_t in + let indices = res |> U.head_and_args_full |> snd in + let env = args |> List.fold_left + (fun env ({binder_bv=x}) -> push_term_var env x (mkApp(mk_term_projector_name l x, [xx]))) + env in + let indices, decls' = encode_args indices env in + if List.length indices <> List.length vars + then failwith "Impossible"; + let eqs = + if is_injective_on_params + || Options.ext_getv "compat:injectivity" <> "" + then List.map2 (fun v a -> mkEq(mkFreeV v, a)) vars indices + else ( + //only injectivity on indices + let num_params = List.length tps in + let _var_params, var_indices = List.splitAt num_params vars in + let _i_params, indices = List.splitAt num_params indices in + List.map2 (fun v a -> mkEq(mkFreeV v, a)) var_indices indices + ) + in + mkOr(out, mkAnd(mk_data_tester env l xx, eqs |> mk_and_l)), decls@decls') + (mkFalse, []) + in + let ffsym, ff = fresh_fvar env.current_module_name "f" Fuel_sort in + let fuel_guarded_inversion = + let xx_has_type_sfuel = + if List.length datas > 1 + then mk_HasTypeFuel (mkApp("SFuel", [ff])) xx tapp + else mk_HasTypeFuel ff xx tapp //no point requiring non-zero fuel if there are no disjunctions + in + Util.mkAssume( + mkForall + (Ident.range_of_lid t) + ([[xx_has_type_sfuel]], + add_fuel (mk_fv (ffsym, Fuel_sort)) (mk_fv (xxsym, Term_sort)::vars), + mkImp(xx_has_type_sfuel, data_ax)), + Some "inversion axiom", //this name matters! see Sig_bundle case near line 1493 + (varops.mk_unique ("fuel_guarded_inversion_"^(string_of_lid t)))) + in + decls + @([fuel_guarded_inversion] |> mk_decls_trivial) + ) + in + let formals, res = + let k = + match tps with + | [] -> k + | _ -> S.mk (Tm_arrow {bs=tps; comp=S.mk_Total k}) k.pos + in + let k = norm_before_encoding env k in + U.arrow_formals k + in + let vars, guards, env', binder_decls, _ = encode_binders None formals env in + let arity = List.length vars in + let tname, ttok, env = new_term_constant_and_tok_from_lid env t arity in + let ttok_tm = mkApp(ttok, []) in + let guard = mk_and_l guards in + let tapp = mkApp(tname, List.map mkFreeV vars) in //arity ok + let decls, env = + //See: https://github.com/FStarLang/FStar/commit/b75225bfbe427c8aef5b59f70ff6d79aa014f0b4 + //See: https://github.com/FStarLang/FStar/issues/349 + let tname_decl = + constructor_or_logic_type_decl + { + constr_name = tname; + constr_fields = vars |> List.map (fun fv -> {field_name=tname^fv_name fv; field_sort=fv_sort fv; field_projectible=false}) ; + //The field_projectible=false above is extremely important; it makes sure that type-formers are not injective + constr_sort=Term_sort; + constr_id=Some (varops.next_id()) + } + in + let tok_decls, env = + match vars with + | [] -> [], push_free_var env t arity tname (Some <| mkApp(tname, [])) + | _ -> + let ttok_decl = Term.DeclFun(ttok, [], Term_sort, Some "token") in + let ttok_fresh = Term.fresh_token (ttok, Term_sort) (varops.next_id()) in + let ttok_app = mk_Apply ttok_tm vars in + let pats = [[ttok_app]; [tapp]] in + // These patterns allow rewriting (ApplyT T@tok args) to (T args) and vice versa + // This seems necessary for some proofs, but the bidirectional rewriting may be inefficient + let name_tok_corr = + Util.mkAssume(mkForall' (Ident.range_of_lid t) (pats, None, vars, mkEq(ttok_app, tapp)), + Some "name-token correspondence", + ("token_correspondence_"^ttok)) in + [ttok_decl; ttok_fresh; name_tok_corr], env + in + tname_decl@tok_decls, env + in + let kindingAx = + let k, decls = encode_term_pred None res env' tapp in + let karr = + if List.length formals > 0 + then [Util.mkAssume(mk_tester "Tm_arrow" (mk_PreType ttok_tm), Some "kinding", ("pre_kinding_"^ttok))] + else [] + in + let rng = Ident.range_of_lid t in + let tot_fun_axioms = EncodeTerm.isTotFun_axioms rng ttok_tm vars (List.map (fun _ -> mkTrue) vars) true in + decls@(karr@[Util.mkAssume(mkAnd(tot_fun_axioms, mkForall rng ([[tapp]], vars, mkImp(guard, k))), + None, + ("kinding_"^ttok))] |> mk_decls_trivial) + in + let aux = + kindingAx + @(inversion_axioms env tapp vars) + @([pretype_axiom (Ident.range_of_lid t) env tapp vars] |> mk_decls_trivial) + in + (decls |> mk_decls_trivial)@binder_decls@aux, env + +let encode_datacon (is_injective_on_tparams:bool) (env:env_t) (se:sigelt) +: decls_t * env_t += let Sig_datacon {lid=d; t; num_ty_params=n_tps; mutuals} = se.sigel in + let quals = se.sigquals in + let t = norm_before_encoding env t in + let formals, t_res = U.arrow_formals t in + let arity = List.length formals in + let ddconstrsym, ddtok, env = new_term_constant_and_tok_from_lid env d arity in + let ddtok_tm = mkApp(ddtok, []) in + let fuel_var, fuel_tm = fresh_fvar env.current_module_name "f" Fuel_sort in + let s_fuel_tm = mkApp("SFuel", [fuel_tm]) in + let vars, guards, env', binder_decls, names = encode_binders (Some fuel_tm) formals env in + let fields = names |> List.mapi (fun n x -> + { field_name=mk_term_projector_name d x; + field_sort=Term_sort; + field_projectible=true }) + in + let datacons = + {constr_name=ddconstrsym; + constr_fields=fields; + constr_sort=Term_sort; + constr_id=Some (varops.next_id()) + } |> Term.constructor_to_decl (Ident.range_of_lid d) in + let app = mk_Apply ddtok_tm vars in + let guard = mk_and_l guards in + let xvars = List.map mkFreeV vars in + let dapp = mkApp(ddconstrsym, xvars) in //arity ok; |xvars| = |formals| = arity + + let tok_typing, decls3 = encode_term_pred None t env ddtok_tm in + let tok_typing = + match fields with + | _::_ -> + let ff = mk_fv ("ty", Term_sort) in + let f = mkFreeV ff in + let vtok_app_l = mk_Apply ddtok_tm [ff] in + let vtok_app_r = mk_Apply f [mk_fv (ddtok, Term_sort)] in + //guard the token typing assumption with a Apply(tok, f) or Apply(f, tok) + //Additionally, the body of the term becomes NoHoist f (HasType tok ...) + // to prevent the Z3 simplifier from hoisting the (HasType tok ...) part out + //Since the top-levels of modules are full of function typed terms + //not guarding it this way causes every typing assumption of an arrow type to be fired immediately + //regardless of whether or not the function is used ... leading to bloat + //these patterns aim to restrict the use of the typing assumption until such point as it is actually needed + mkForall (Ident.range_of_lid d) + ([[vtok_app_l]; [vtok_app_r]], + [ff], + Term.mk_NoHoist f tok_typing) + | _ -> tok_typing in + let ty_pred', t_res_tm, decls_pred = + let t_res_tm, t_res_decls = encode_term t_res env' in + mk_HasTypeWithFuel (Some fuel_tm) dapp t_res_tm, t_res_tm, t_res_decls in + let proxy_fresh = match formals with + | [] -> [] + | _ -> [Term.fresh_token (ddtok, Term_sort) (varops.next_id())] in + + let encode_elim () = + let head, args = U.head_and_args t_res in + match (SS.compress head).n with + | Tm_uinst({n=Tm_fvar fv}, _) + | Tm_fvar fv -> + let encoded_head_fvb = lookup_free_var_name env' fv.fv_name in + let encoded_args, arg_decls = encode_args args env' in + let guards_for_parameter (orig_arg:S.term)(arg:term) xv = + let fv = + match arg.tm with + | FreeV fv -> fv + | _ -> + Errors.raise_error (Errors.Fatal_NonVariableInductiveTypeParameter, + BU.format1 "Inductive type parameter %s must be a variable ; \ + You may want to change it to an index." + (FStar.Syntax.Print.term_to_string orig_arg)) orig_arg.pos + in + let guards = guards |> List.collect (fun g -> + if List.contains fv (Term.free_variables g) + then [Term.subst g fv xv] + else []) + in + mk_and_l guards + in + let _, arg_vars, elim_eqns_or_guards, _ = + List.fold_left + (fun (env, arg_vars, eqns_or_guards, i) (orig_arg, arg) -> + let _, xv, env = gen_term_var env (S.new_bv None tun) in + (* we only get equations induced on the type indices, not parameters; *) + (* Also see https://github.com/FStarLang/FStar/issues/349 *) + let eqns = + if i < n_tps + then guards_for_parameter (fst orig_arg) arg xv::eqns_or_guards + else mkEq(arg, xv)::eqns_or_guards + in + (env, xv::arg_vars, eqns, i + 1)) + (env', [], [], 0) + (FStar.Compiler.List.zip args encoded_args) + in + let arg_vars = List.rev arg_vars in + let ty = maybe_curry_fvb fv.fv_name.p encoded_head_fvb arg_vars in + let xvars = List.map mkFreeV vars in + let dapp = mkApp(ddconstrsym, xvars) in //arity ok; |xvars| = |formals| = arity + let ty_pred = mk_HasTypeWithFuel (Some s_fuel_tm) dapp ty in + let arg_binders = List.map fv_of_term arg_vars in + let typing_inversion = + Util.mkAssume(mkForall (Ident.range_of_lid d) ([[ty_pred]], + add_fuel (mk_fv (fuel_var, Fuel_sort)) (vars@arg_binders), + mkImp(ty_pred, mk_and_l (elim_eqns_or_guards@guards))), + Some "data constructor typing elim", + ("data_elim_" ^ ddconstrsym)) in + let lex_t = mkFreeV <| mk_fv (string_of_lid Const.lex_t_lid, Term_sort) in + let subterm_ordering = + (* subterm ordering *) + let prec = + vars + |> List.mapi (fun i v -> + (* it's a parameter, so it's inaccessible and no need for a sub-term ordering on it *) + if i < n_tps + then [] + else [mk_Precedes lex_t lex_t (mkFreeV v) dapp]) + |> List.flatten + in + Util.mkAssume(mkForall (Ident.range_of_lid d) + ([[ty_pred]], + add_fuel (mk_fv (fuel_var, Fuel_sort)) (vars@arg_binders), + mkImp(ty_pred, mk_and_l prec)), + Some "subterm ordering", + ("subterm_ordering_"^ddconstrsym)) + in + let codomain_ordering, codomain_decls = + let _, formals' = BU.first_N n_tps formals in (* no codomain ordering for the parameters *) + let _, vars' = BU.first_N n_tps vars in + let norm t = + N.unfold_whnf' [Env.AllowUnboundUniverses; + Env.EraseUniverses; + Env.Unascribe; + //we don't know if this will terminate; so don't do recursive steps + Env.Exclude Env.Zeta] + env'.tcenv + t + in + let warn_compat () = + FStar.Errors.log_issue + (S.range_of_fv fv) + (FStar.Errors.Warning_DeprecatedGeneric, + "Using 'compat:2954' to use a permissive encoding of the subterm ordering on the codomain of a constructor.\n\ + This is deprecated and will be removed in a future version of F*.") + in + let codomain_prec_l, cod_decls = + List.fold_left2 + (fun (codomain_prec_l, cod_decls) formal var -> + let rec binder_and_codomain_type t = + let t = U.unrefine t in + match (SS.compress t).n with + | Tm_arrow _ -> + let bs, c = U.arrow_formals_comp (U.unrefine t) in + begin + match bs with + | [] -> None + | _ when not (U.is_tot_or_gtot_comp c) -> None + | _ -> + if U.is_lemma_comp c + then None //not useful for lemmas + else + let t = U.unrefine (U.comp_result c) in + let t = norm t in + if is_type t || U.is_sub_singleton t + then None //ordering on Type and squashed values is not useful + else ( + let head, _ = U.head_and_args_full t in + match (U.un_uinst head).n with + | Tm_fvar fv -> + if BU.for_some (S.fv_eq_lid fv) mutuals + then Some (bs, c) + else if Options.ext_getv "compat:2954" <> "" + then (warn_compat(); Some (bs, c)) //compatibility mode + else None + | _ -> + if Options.ext_getv "compat:2954" <> "" + then (warn_compat(); Some (bs, c)) //compatibility mode + else None + ) + end + | _ -> + let head, _ = U.head_and_args t in + let t' = norm t in + let head', _ = U.head_and_args t' in + match U.eq_tm head head' with + | U.Equal -> None //no progress after whnf + | U.NotEqual -> binder_and_codomain_type t' + | _ -> + //Did we actually make progress? Be conservative to avoid an infinite loop + match (SS.compress head).n with + | Tm_fvar _ + | Tm_name _ + | Tm_uinst _ -> + //The underlying name must have changed, otherwise we would have got Equal + //so, we made some progress + binder_and_codomain_type t' + | _ -> + //unclear if we made progress or not + None + + in + match binder_and_codomain_type formal.binder_bv.sort with + | None -> + codomain_prec_l, cod_decls + | Some (bs, c) -> + //var bs << D ... var ... + let bs', guards', _env', bs_decls, _ = encode_binders None bs env' in + let fun_app = mk_Apply (mkFreeV var) bs' in + mkForall (Ident.range_of_lid d) + ([[mk_Precedes lex_t lex_t fun_app dapp]], + bs', + //need to use ty_pred' here, to avoid variable capture + //Note, ty_pred' is indexed by fuel, not S_fuel + //That's ok, since the outer pattern is guarded on S_fuel + mkImp (mk_and_l (ty_pred'::guards'), + mk_Precedes lex_t lex_t fun_app dapp)) + :: codomain_prec_l, + bs_decls @ cod_decls) + ([],[]) + formals' + vars' + in + match codomain_prec_l with + | [] -> + [], cod_decls + | _ -> + [Util.mkAssume(mkForall (Ident.range_of_lid d) + ([[ty_pred]],//we use ty_pred here as the pattern, which has an S_fuel guard + add_fuel (mk_fv (fuel_var, Fuel_sort)) (vars@arg_binders), + mk_and_l codomain_prec_l), + Some "well-founded ordering on codomain", + ("well_founded_ordering_on_codomain_"^ddconstrsym))], + cod_decls + in + arg_decls @ codomain_decls, + [typing_inversion; subterm_ordering] @ codomain_ordering + + | _ -> + Errors.log_issue se.sigrng + (Errors.Warning_ConstructorBuildsUnexpectedType, + BU.format2 "Constructor %s builds an unexpected type %s\n" + (Print.lid_to_string d) (Print.term_to_string head)); + [], [] + in + let decls2, elim = encode_elim () in + let data_cons_typing_intro_decl = + // + //AR: + // + //Typing intro for the data constructor + // + //We do a bit of manipulation for type indices + //Consider the Cons data constructor of a length-indexed vector type: + // type vector : nat -> Type = | Emp : vector 0 + // | Cons: n:nat -> hd:nat -> tl:vec n -> vec (n+1) + // + //So far we have + // ty_pred' = HasTypeFuel f (Cons n hd tl) (vector (n+1)) + // vars = n, hd, tl + // guard = And of typing guards for n, hd, tl (i.e. (HasType n nat) etc.) + // + //If we emitted the straightforward typing axiom: + // forall n hd tl. HasTypeFuel f (Cons n hd tl) (vector (n+1)) + //with pattern + // HasTypeFuel f (Cons n hd tl) (vecor (n+1)) + // + //It results in too restrictive a pattern, + //Specifically, if we need to prove HasTypeFuel f (Cons 0 1 Emp) (vector 1), + // the axiom will not fire, since the pattern is specifically looking for + // (n+1) in the resulting vector type, whereas here we have a term 1, + // which is not addition syntactically + // + //So we do a little bit of surgery below to emit an axiom of the form: + // forall n hd tl m. m = n + 1 ==> HasTypeFuel f (Cons n hd tl) (vector m) + //where m is a fresh variable + // + //Also see #2456 + // + let ty_pred', vars, guard = + match t_res_tm.tm with + | App (op, args) -> + //iargs are index arguments in the return type of the data constructor + let targs, iargs = List.splitAt n_tps args in + //fresh vars for iargs + let fresh_ivars, fresh_iargs = + iargs |> List.map (fun _ -> fresh_fvar env.current_module_name "i" Term_sort) + |> List.split in + //equality guards + let additional_guards = + mk_and_l (List.map2 (fun a fresh_a -> mkEq (a, fresh_a)) iargs fresh_iargs) in + + mk_HasTypeWithFuel + (Some fuel_tm) + dapp + ({t_res_tm with tm = App (op, targs@fresh_iargs)}), + + vars@(fresh_ivars |> List.map (fun s -> mk_fv (s, Term_sort))), + + mkAnd (guard, additional_guards) + + | _ -> ty_pred', vars, guard in //When will this case arise? + + Util.mkAssume(mkForall (Ident.range_of_lid d) + ([[ty_pred']],add_fuel (mk_fv (fuel_var, Fuel_sort)) vars, mkImp(guard, ty_pred')), + Some "data constructor typing intro", + ("data_typing_intro_"^ddtok)) in + + let g = binder_decls + @decls2 + @decls3 + @([Term.DeclFun(ddtok, [], Term_sort, Some (BU.format1 "data constructor proxy: %s" (Print.lid_to_string d)))] + @proxy_fresh |> mk_decls_trivial) + @decls_pred + @([Util.mkAssume(tok_typing, Some "typing for data constructor proxy", ("typing_tok_"^ddtok)); + Util.mkAssume(mkForall (Ident.range_of_lid d) + ([[app]], vars, + mkEq(app, dapp)), Some "equality for proxy", ("equality_tok_"^ddtok)); + data_cons_typing_intro_decl; + ]@elim |> mk_decls_trivial) in + (datacons |> mk_decls_trivial) @ g, env + + let rec encode_sigelt (env:env_t) (se:sigelt) : (decls_t * env_t) = let nm = Print.sigelt_to_string_short se in let g, env = Errors.with_ctx (BU.format1 "While encoding top-level declaration `%s`" @@ -1214,549 +1750,69 @@ and encode_sigelt' (env:env_t) (se:sigelt) : (decls_t * env_t) = encode_top_level_let env (is_rec, bindings) se.sigquals | Sig_bundle {ses} -> - let g, env = encode_sigelts env ses in - let g', inversions = List.fold_left (fun (g', inversions) elt -> - let elt_g', elt_inversions = elt.decls |> List.partition (function - | Term.Assume({assumption_caption=Some "inversion axiom"}) -> false - | _ -> true) in - g' @ [ { elt with decls = elt_g' } ], inversions @ elt_inversions - ) ([], []) g in - let decls, elts, rest = List.fold_left (fun (decls, elts, rest) elt -> - if elt.key |> BU.is_some && List.existsb (function | Term.DeclFun _ -> true | _ -> false) elt.decls - then decls, elts@[elt], rest - else let elt_decls, elt_rest = elt.decls |> List.partition (function - | Term.DeclFun _ -> true - | _ -> false) in - decls @ elt_decls, elts, rest @ [ { elt with decls = elt_rest }] - ) ([], [], []) g' in - (decls |> mk_decls_trivial) @ elts @ rest @ (inversions |> mk_decls_trivial), env - - | Sig_inductive_typ {lid=t; - us=universe_names; - params=tps; - t=k; - ds=datas} -> - let t_lid = t in - let tcenv = env.tcenv in - let is_injective_on_params = - let usubst, uvs = SS.univ_var_opening universe_names in - let env, tps, k = - Env.push_univ_vars tcenv uvs, - SS.subst_binders usubst tps, - SS.subst (SS.shift_subst (List.length tps) usubst) k - in - let tps, k = SS.open_term tps k in - let _, k = U.arrow_formals k in //don't care about indices here - let tps, env_tps, _, us = TcTerm.tc_binders env tps in - let u_k = - TcTerm.level_of_type - env_tps - (S.mk_Tm_app - (S.fvar t None) - (snd (U.args_of_binders tps)) - (Ident.range_of_lid t)) - k - in - //BU.print2 "Universe of tycon: %s : %s\n" (Ident.string_of_lid t) (Print.univ_to_string u_k); - let rec universe_leq u v = - match u, v with - | U_zero, _ -> true - | U_succ u0, U_succ v0 -> universe_leq u0 v0 - | U_name u0, U_name v0 -> Ident.ident_equals u0 v0 - | U_name _, U_succ v0 -> universe_leq u v0 - | U_max us, _ -> us |> BU.for_all (fun u -> universe_leq u v) - | _, U_max vs -> vs |> BU.for_some (universe_leq u) - | U_unknown, _ - | _, U_unknown - | U_unif _, _ - | _, U_unif _ -> failwith (BU.format3 "Impossible: Unresolved or unknown universe in inductive type %s (%s, %s)" - (Ident.string_of_lid t) - (Print.univ_to_string u) - (Print.univ_to_string v)) - | _ -> false - in - let u_leq_u_k u = - let u = N.normalize_universe env_tps u in - universe_leq u u_k - in - let tp_ok (tp:S.binder) (u_tp:universe) = - let t_tp = tp.binder_bv.sort in - if u_leq_u_k u_tp - then true - else ( - let t_tp = - N.normalize - [Unrefine; Unascribe; Unmeta; - Primops; HNF; UnfoldUntil delta_constant; Beta] - env_tps t_tp - in - let formals, t = U.arrow_formals t_tp in - let _, _, _, u_formals = TcTerm.tc_binders env_tps formals in - let inj = BU.for_all (fun u_formal -> u_leq_u_k u_formal) u_formals in - if inj - then ( - match (SS.compress t).n with - | Tm_type u -> - (* retain injectivity for parameters that are type functions - from small universes (i.e., all formals are smaller than the constructed type) - to a universe <= the universe of the constructed type. - See BugBoxInjectivity.fst *) - u_leq_u_k u - // | Tm_name _ -> (* this is a value of another type parameter in scope *) - // true - | _ -> - false - ) - else ( - false - ) - - ) - in - List.forall2 tp_ok tps us - in - if Env.debug env.tcenv <| Options.Other "SMTEncoding" - then BU.print2 "%s injectivity for %s\n" - (if is_injective_on_params then "YES" else "NO") - (Ident.string_of_lid t); - let quals = se.sigquals in - let is_logical = quals |> BU.for_some (function Logic | Assumption -> true | _ -> false) in - let constructor_or_logic_type_decl (c:constructor_t) = - if is_logical - then [Term.DeclFun(c.constr_name, c.constr_fields |> List.map (fun f -> f.field_sort), Term_sort, None)] - else constructor_to_decl (Ident.range_of_lid t) c in - let inversion_axioms env tapp vars = - if datas |> BU.for_some (fun l -> Env.try_lookup_lid env.tcenv l |> Option.isNone) //Q: Why would this happen? - then [] - else - let xxsym, xx = fresh_fvar env.current_module_name "x" Term_sort in - let data_ax, decls = datas |> List.fold_left (fun (out, decls) l -> - let _, data_t = Env.lookup_datacon env.tcenv l in - let args, res = U.arrow_formals data_t in - let indices = res |> U.head_and_args_full |> snd in - let env = args |> List.fold_left - (fun env ({binder_bv=x}) -> push_term_var env x (mkApp(mk_term_projector_name l x, [xx]))) - env in - let indices, decls' = encode_args indices env in - if List.length indices <> List.length vars - then failwith "Impossible"; - let eqs = - if is_injective_on_params - || Options.ext_getv "compat:injectivity" <> "" - then List.map2 (fun v a -> mkEq(mkFreeV v, a)) vars indices - else ( - //only injectivity on indices - let num_params = List.length tps in - let _var_params, var_indices = List.splitAt num_params vars in - let _i_params, indices = List.splitAt num_params indices in - List.map2 (fun v a -> mkEq(mkFreeV v, a)) var_indices indices - ) - in - mkOr(out, mkAnd(mk_data_tester env l xx, eqs |> mk_and_l)), decls@decls') (mkFalse, []) in - let ffsym, ff = fresh_fvar env.current_module_name "f" Fuel_sort in - let fuel_guarded_inversion = - let xx_has_type_sfuel = - if List.length datas > 1 - then mk_HasTypeFuel (mkApp("SFuel", [ff])) xx tapp - else mk_HasTypeFuel ff xx tapp in //no point requiring non-zero fuel if there are no disjunctions - Util.mkAssume(mkForall (Ident.range_of_lid t) ([[xx_has_type_sfuel]], add_fuel (mk_fv (ffsym, Fuel_sort)) (mk_fv (xxsym, Term_sort)::vars), - mkImp(xx_has_type_sfuel, data_ax)), - Some "inversion axiom", //this name matters! see Sig_bundle case near line 1493 - (varops.mk_unique ("fuel_guarded_inversion_"^(string_of_lid t)))) in - decls - @([fuel_guarded_inversion] |> mk_decls_trivial) in - - let formals, res = - let k = - match tps with - | [] -> k - | _ -> S.mk (Tm_arrow {bs=tps; comp=S.mk_Total k}) k.pos - in - let k = norm_before_encoding env k in - U.arrow_formals k - in - - let vars, guards, env', binder_decls, _ = encode_binders None formals env in - let arity = List.length vars in - let tname, ttok, env = new_term_constant_and_tok_from_lid env t arity in - let ttok_tm = mkApp(ttok, []) in - let guard = mk_and_l guards in - let tapp = mkApp(tname, List.map mkFreeV vars) in //arity ok - let decls, env = - //See: https://github.com/FStarLang/FStar/commit/b75225bfbe427c8aef5b59f70ff6d79aa014f0b4 - //See: https://github.com/FStarLang/FStar/issues/349 - let tname_decl = - constructor_or_logic_type_decl - { - constr_name = tname; - constr_fields = vars |> List.map (fun fv -> {field_name=tname^fv_name fv; field_sort=fv_sort fv; field_projectible=false}) ; - //The field_projectible=false above is extremely important; it makes sure that type-formers are not injective - constr_sort=Term_sort; - constr_id=Some (varops.next_id()) - } - in - let tok_decls, env = - match vars with - | [] -> [], push_free_var env t arity tname (Some <| mkApp(tname, [])) - | _ -> - let ttok_decl = Term.DeclFun(ttok, [], Term_sort, Some "token") in - let ttok_fresh = Term.fresh_token (ttok, Term_sort) (varops.next_id()) in - let ttok_app = mk_Apply ttok_tm vars in - let pats = [[ttok_app]; [tapp]] in - // These patterns allow rewriting (ApplyT T@tok args) to (T args) and vice versa - // This seems necessary for some proofs, but the bidirectional rewriting may be inefficient - let name_tok_corr = Util.mkAssume(mkForall' (Ident.range_of_lid t) (pats, None, vars, mkEq(ttok_app, tapp)), - Some "name-token correspondence", - ("token_correspondence_"^ttok)) in - [ttok_decl; ttok_fresh; name_tok_corr], env in - tname_decl@tok_decls, env in - let kindingAx = - let k, decls = encode_term_pred None res env' tapp in - let karr = - if List.length formals > 0 - then [Util.mkAssume(mk_tester "Tm_arrow" (mk_PreType ttok_tm), Some "kinding", ("pre_kinding_"^ttok))] - else [] - in - let rng = Ident.range_of_lid t in - let tot_fun_axioms = - EncodeTerm.isTotFun_axioms rng ttok_tm vars (List.map (fun _ -> mkTrue) vars) true + let tycon = List.tryFind (fun se -> Sig_inductive_typ? se.sigel) ses in + let is_injective_on_params = + match tycon with + | None -> failwith "Impossible: Sig_bundle without a Sig_inductive_typ" + | Some se -> + is_sig_inductive_injective_on_params env se + in + let g, env = + ses |> + List.fold_left + (fun (g, env) se -> + let g', env = + match se.sigel with + | Sig_inductive_typ _ -> + encode_sig_inductive is_injective_on_params env se + | Sig_datacon _ -> + encode_datacon is_injective_on_params env se + | _ -> + encode_sigelt env se in - - decls@(karr@[Util.mkAssume(mkAnd(tot_fun_axioms, mkForall rng ([[tapp]], vars, mkImp(guard, k))), None, ("kinding_"^ttok))] - |> mk_decls_trivial) in - let aux = - kindingAx - @(inversion_axioms env tapp vars) - @([pretype_axiom (Ident.range_of_lid t) env tapp vars] |> mk_decls_trivial) in - - let g = (decls |> mk_decls_trivial) - @binder_decls - @aux in - g, env - - | Sig_datacon {lid=d; t; num_ty_params=n_tps; mutuals} -> - let quals = se.sigquals in - let t = norm_before_encoding env t in - let formals, t_res = U.arrow_formals t in - let arity = List.length formals in - let ddconstrsym, ddtok, env = new_term_constant_and_tok_from_lid env d arity in - let ddtok_tm = mkApp(ddtok, []) in - let fuel_var, fuel_tm = fresh_fvar env.current_module_name "f" Fuel_sort in - let s_fuel_tm = mkApp("SFuel", [fuel_tm]) in - let vars, guards, env', binder_decls, names = encode_binders (Some fuel_tm) formals env in - let fields = names |> List.mapi (fun n x -> - { field_name=mk_term_projector_name d x; - field_sort=Term_sort; - field_projectible=true }) - in - let datacons = - {constr_name=ddconstrsym; - constr_fields=fields; - constr_sort=Term_sort; - constr_id=Some (varops.next_id()) - } |> Term.constructor_to_decl (Ident.range_of_lid d) in - let app = mk_Apply ddtok_tm vars in - let guard = mk_and_l guards in - let xvars = List.map mkFreeV vars in - let dapp = mkApp(ddconstrsym, xvars) in //arity ok; |xvars| = |formals| = arity - - let tok_typing, decls3 = encode_term_pred None t env ddtok_tm in - let tok_typing = - match fields with - | _::_ -> - let ff = mk_fv ("ty", Term_sort) in - let f = mkFreeV ff in - let vtok_app_l = mk_Apply ddtok_tm [ff] in - let vtok_app_r = mk_Apply f [mk_fv (ddtok, Term_sort)] in - //guard the token typing assumption with a Apply(tok, f) or Apply(f, tok) - //Additionally, the body of the term becomes NoHoist f (HasType tok ...) - // to prevent the Z3 simplifier from hoisting the (HasType tok ...) part out - //Since the top-levels of modules are full of function typed terms - //not guarding it this way causes every typing assumption of an arrow type to be fired immediately - //regardless of whether or not the function is used ... leading to bloat - //these patterns aim to restrict the use of the typing assumption until such point as it is actually needed - mkForall (Ident.range_of_lid d) - ([[vtok_app_l]; [vtok_app_r]], - [ff], - Term.mk_NoHoist f tok_typing) - | _ -> tok_typing in - let ty_pred', t_res_tm, decls_pred = - let t_res_tm, t_res_decls = encode_term t_res env' in - mk_HasTypeWithFuel (Some fuel_tm) dapp t_res_tm, t_res_tm, t_res_decls in - let proxy_fresh = match formals with - | [] -> [] - | _ -> [Term.fresh_token (ddtok, Term_sort) (varops.next_id())] in - - let encode_elim () = - let head, args = U.head_and_args t_res in - match (SS.compress head).n with - | Tm_uinst({n=Tm_fvar fv}, _) - | Tm_fvar fv -> - let encoded_head_fvb = lookup_free_var_name env' fv.fv_name in - let encoded_args, arg_decls = encode_args args env' in - let guards_for_parameter (orig_arg:S.term)(arg:term) xv = - let fv = - match arg.tm with - | FreeV fv -> fv - | _ -> - Errors.raise_error (Errors.Fatal_NonVariableInductiveTypeParameter, - BU.format1 "Inductive type parameter %s must be a variable ; \ - You may want to change it to an index." - (FStar.Syntax.Print.term_to_string orig_arg)) orig_arg.pos - in - let guards = guards |> List.collect (fun g -> - if List.contains fv (Term.free_variables g) - then [Term.subst g fv xv] - else []) - in - mk_and_l guards - in - let _, arg_vars, elim_eqns_or_guards, _ = - List.fold_left - (fun (env, arg_vars, eqns_or_guards, i) (orig_arg, arg) -> - let _, xv, env = gen_term_var env (S.new_bv None tun) in - (* we only get equations induced on the type indices, not parameters; *) - (* Also see https://github.com/FStarLang/FStar/issues/349 *) - let eqns = - if i < n_tps - then guards_for_parameter (fst orig_arg) arg xv::eqns_or_guards - else mkEq(arg, xv)::eqns_or_guards - in - (env, xv::arg_vars, eqns, i + 1)) - (env', [], [], 0) - (FStar.Compiler.List.zip args encoded_args) + g@g', env) + ([], env) + in + //reorder the generated decls in proper def-use order, + //i.e, declare all the function symbols first + //1. move the inversions last; they rely on all the symbols + let g', inversions = + List.fold_left + (fun (g', inversions) elt -> + let elt_g', elt_inversions = + elt.decls |> + List.partition + (function + | Term.Assume({assumption_caption=Some "inversion axiom"}) -> false + | _ -> true) in - let arg_vars = List.rev arg_vars in - let ty = maybe_curry_fvb fv.fv_name.p encoded_head_fvb arg_vars in - let xvars = List.map mkFreeV vars in - let dapp = mkApp(ddconstrsym, xvars) in //arity ok; |xvars| = |formals| = arity - let ty_pred = mk_HasTypeWithFuel (Some s_fuel_tm) dapp ty in - let arg_binders = List.map fv_of_term arg_vars in - let typing_inversion = - Util.mkAssume(mkForall (Ident.range_of_lid d) ([[ty_pred]], - add_fuel (mk_fv (fuel_var, Fuel_sort)) (vars@arg_binders), - mkImp(ty_pred, mk_and_l (elim_eqns_or_guards@guards))), - Some "data constructor typing elim", - ("data_elim_" ^ ddconstrsym)) in - let lex_t = mkFreeV <| mk_fv (string_of_lid Const.lex_t_lid, Term_sort) in - let subterm_ordering = - (* subterm ordering *) - let prec = - vars - |> List.mapi (fun i v -> - (* it's a parameter, so it's inaccessible and no need for a sub-term ordering on it *) - if i < n_tps - then [] - else [mk_Precedes lex_t lex_t (mkFreeV v) dapp]) - |> List.flatten - in - Util.mkAssume(mkForall (Ident.range_of_lid d) - ([[ty_pred]], - add_fuel (mk_fv (fuel_var, Fuel_sort)) (vars@arg_binders), - mkImp(ty_pred, mk_and_l prec)), - Some "subterm ordering", - ("subterm_ordering_"^ddconstrsym)) - in - let codomain_ordering, codomain_decls = - let _, formals' = BU.first_N n_tps formals in (* no codomain ordering for the parameters *) - let _, vars' = BU.first_N n_tps vars in - let norm t = - N.unfold_whnf' [Env.AllowUnboundUniverses; - Env.EraseUniverses; - Env.Unascribe; - //we don't know if this will terminate; so don't do recursive steps - Env.Exclude Env.Zeta] - env'.tcenv - t - in - let warn_compat () = - FStar.Errors.log_issue - (S.range_of_fv fv) - (FStar.Errors.Warning_DeprecatedGeneric, - "Using 'compat:2954' to use a permissive encoding of the subterm ordering on the codomain of a constructor.\n\ - This is deprecated and will be removed in a future version of F*.") - in - let codomain_prec_l, cod_decls = - List.fold_left2 - (fun (codomain_prec_l, cod_decls) formal var -> - let rec binder_and_codomain_type t = - let t = U.unrefine t in - match (SS.compress t).n with - | Tm_arrow _ -> - let bs, c = U.arrow_formals_comp (U.unrefine t) in - begin - match bs with - | [] -> None - | _ when not (U.is_tot_or_gtot_comp c) -> None - | _ -> - if U.is_lemma_comp c - then None //not useful for lemmas - else - let t = U.unrefine (U.comp_result c) in - let t = norm t in - if is_type t || U.is_sub_singleton t - then None //ordering on Type and squashed values is not useful - else ( - let head, _ = U.head_and_args_full t in - match (U.un_uinst head).n with - | Tm_fvar fv -> - if BU.for_some (S.fv_eq_lid fv) mutuals - then Some (bs, c) - else if Options.ext_getv "compat:2954" <> "" - then (warn_compat(); Some (bs, c)) //compatibility mode - else None - | _ -> - if Options.ext_getv "compat:2954" <> "" - then (warn_compat(); Some (bs, c)) //compatibility mode - else None - ) - end - | _ -> - let head, _ = U.head_and_args t in - let t' = norm t in - let head', _ = U.head_and_args t' in - match U.eq_tm head head' with - | U.Equal -> None //no progress after whnf - | U.NotEqual -> binder_and_codomain_type t' - | _ -> - //Did we actually make progress? Be conservative to avoid an infinite loop - match (SS.compress head).n with - | Tm_fvar _ - | Tm_name _ - | Tm_uinst _ -> - //The underlying name must have changed, otherwise we would have got Equal - //so, we made some progress - binder_and_codomain_type t' - | _ -> - //unclear if we made progress or not - None - - in - match binder_and_codomain_type formal.binder_bv.sort with - | None -> - codomain_prec_l, cod_decls - | Some (bs, c) -> - //var bs << D ... var ... - let bs', guards', _env', bs_decls, _ = encode_binders None bs env' in - let fun_app = mk_Apply (mkFreeV var) bs' in - mkForall (Ident.range_of_lid d) - ([[mk_Precedes lex_t lex_t fun_app dapp]], - bs', - //need to use ty_pred' here, to avoid variable capture - //Note, ty_pred' is indexed by fuel, not S_fuel - //That's ok, since the outer pattern is guarded on S_fuel - mkImp (mk_and_l (ty_pred'::guards'), - mk_Precedes lex_t lex_t fun_app dapp)) - :: codomain_prec_l, - bs_decls @ cod_decls) - ([],[]) - formals' - vars' - in - match codomain_prec_l with - | [] -> - [], cod_decls - | _ -> - [Util.mkAssume(mkForall (Ident.range_of_lid d) - ([[ty_pred]],//we use ty_pred here as the pattern, which has an S_fuel guard - add_fuel (mk_fv (fuel_var, Fuel_sort)) (vars@arg_binders), - mk_and_l codomain_prec_l), - Some "well-founded ordering on codomain", - ("well_founded_ordering_on_codomain_"^ddconstrsym))], - cod_decls + g' @ [ { elt with decls = elt_g' } ], + inversions @ elt_inversions) + ([], []) + g + in + //2. decls are all the function symbol declarations + // elts: not sure what this represents + // rest: all the non-declarations, excepting the inversion axiom which is already identified above + let decls, elts, rest = + List.fold_left + (fun (decls, elts, rest) elt -> + if BU.is_some elt.key //NS: Not sure what this case is for + && List.existsb (function | Term.DeclFun _ -> true | _ -> false) elt.decls + then decls, elts@[elt], rest + else ( //Pull the function symbol decls to the front + let elt_decls, elt_rest = + elt.decls |> + List.partition + (function + | Term.DeclFun _ -> true + | _ -> false) in - arg_decls @ codomain_decls, - [typing_inversion; subterm_ordering] @ codomain_ordering - - | _ -> - Errors.log_issue se.sigrng - (Errors.Warning_ConstructorBuildsUnexpectedType, - BU.format2 "Constructor %s builds an unexpected type %s\n" - (Print.lid_to_string d) (Print.term_to_string head)); - [], [] - in - let decls2, elim = encode_elim () in - let data_cons_typing_intro_decl = - // - //AR: - // - //Typing intro for the data constructor - // - //We do a bit of manipulation for type indices - //Consider the Cons data constructor of a length-indexed vector type: - // type vector : nat -> Type = | Emp : vector 0 - // | Cons: n:nat -> hd:nat -> tl:vec n -> vec (n+1) - // - //So far we have - // ty_pred' = HasTypeFuel f (Cons n hd tl) (vector (n+1)) - // vars = n, hd, tl - // guard = And of typing guards for n, hd, tl (i.e. (HasType n nat) etc.) - // - //If we emitted the straightforward typing axiom: - // forall n hd tl. HasTypeFuel f (Cons n hd tl) (vector (n+1)) - //with pattern - // HasTypeFuel f (Cons n hd tl) (vecor (n+1)) - // - //It results in too restrictive a pattern, - //Specifically, if we need to prove HasTypeFuel f (Cons 0 1 Emp) (vector 1), - // the axiom will not fire, since the pattern is specifically looking for - // (n+1) in the resulting vector type, whereas here we have a term 1, - // which is not addition syntactically - // - //So we do a little bit of surgery below to emit an axiom of the form: - // forall n hd tl m. m = n + 1 ==> HasTypeFuel f (Cons n hd tl) (vector m) - //where m is a fresh variable - // - //Also see #2456 - // - let ty_pred', vars, guard = - match t_res_tm.tm with - | App (op, args) -> - //iargs are index arguments in the return type of the data constructor - let targs, iargs = List.splitAt n_tps args in - //fresh vars for iargs - let fresh_ivars, fresh_iargs = - iargs |> List.map (fun _ -> fresh_fvar env.current_module_name "i" Term_sort) - |> List.split in - //equality guards - let additional_guards = - mk_and_l (List.map2 (fun a fresh_a -> mkEq (a, fresh_a)) iargs fresh_iargs) in - - mk_HasTypeWithFuel - (Some fuel_tm) - dapp - ({t_res_tm with tm = App (op, targs@fresh_iargs)}), - - vars@(fresh_ivars |> List.map (fun s -> mk_fv (s, Term_sort))), - - mkAnd (guard, additional_guards) - - | _ -> ty_pred', vars, guard in //When will this case arise? - - Util.mkAssume(mkForall (Ident.range_of_lid d) - ([[ty_pred']],add_fuel (mk_fv (fuel_var, Fuel_sort)) vars, mkImp(guard, ty_pred')), - Some "data constructor typing intro", - ("data_typing_intro_"^ddtok)) in - - let g = binder_decls - @decls2 - @decls3 - @([Term.DeclFun(ddtok, [], Term_sort, Some (BU.format1 "data constructor proxy: %s" (Print.lid_to_string d)))] - @proxy_fresh |> mk_decls_trivial) - @decls_pred - @([Util.mkAssume(tok_typing, Some "typing for data constructor proxy", ("typing_tok_"^ddtok)); - Util.mkAssume(mkForall (Ident.range_of_lid d) - ([[app]], vars, - mkEq(app, dapp)), Some "equality for proxy", ("equality_tok_"^ddtok)); - data_cons_typing_intro_decl; - ]@elim |> mk_decls_trivial) in - (datacons |> mk_decls_trivial) @ g, env - -and encode_sigelts env ses :(decls_t * env_t) = - ses |> List.fold_left (fun (g, env) se -> - let g', env = encode_sigelt env se in - g@g', env) ([], env) - + decls @ elt_decls, elts, rest @ [ { elt with decls = elt_rest }] + )) + ([], [], []) g' + in + (decls |> mk_decls_trivial) @ elts @ rest @ (inversions |> mk_decls_trivial), env let encode_env_bindings (env:env_t) (bindings:list S.binding) : (decls_t * env_t) = (* Encoding Binding_var and Binding_typ as local constants leads to breakages in hash consing.