diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml index 1357a339791..3b40a356ce6 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml @@ -1174,8 +1174,7 @@ let rec (translate_type_without_decay' : FStar_Compiler_List.map (translate_type_without_decay env1) ts in TTuple uu___ and (translate_type' : env -> FStar_Extraction_ML_Syntax.mlty -> typ) = - fun env1 -> - fun t -> match t with | t1 -> translate_type_without_decay env1 t1 + fun env1 -> fun t -> translate_type_without_decay env1 t and (translate_binders : env -> (Prims.string * FStar_Extraction_ML_Syntax.mlty) Prims.list -> diff --git a/ocaml/fstar-lib/generated/FStar_Interactive_Lsp.ml b/ocaml/fstar-lib/generated/FStar_Interactive_Lsp.ml index d655992f683..2f03d9e8518 100644 --- a/ocaml/fstar-lib/generated/FStar_Interactive_Lsp.ml +++ b/ocaml/fstar-lib/generated/FStar_Interactive_Lsp.ml @@ -509,12 +509,7 @@ let rec (go : FStar_Interactive_Ide_Types.grepl_state -> Prims.int) = let response' = FStar_Interactive_JsonHelper.json_of_response query.FStar_Interactive_JsonHelper.query_id response in - (if false - then - (let uu___3 = FStar_Json.string_of_json response' in - FStar_Compiler_Util.print1_error "<<< %s\n" uu___3) - else (); - FStar_Interactive_JsonHelper.write_jsonrpc response') + FStar_Interactive_JsonHelper.write_jsonrpc response' | FStar_Pervasives_Native.None -> ()); (match state_opt with | FStar_Pervasives.Inl gst' -> go gst' diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml index 53daf28a3a2..ed7eaa866fa 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml @@ -292,6 +292,8 @@ let (must_erase_for_extraction_attr : FStar_Ident.lident) = psconst "must_erase_for_extraction" let (strict_on_arguments_attr : FStar_Ident.lident) = p2l ["FStar"; "Pervasives"; "strict_on_arguments"] +let (strict_on_arguments_unfold_attr : FStar_Ident.lident) = + p2l ["FStar"; "Pervasives"; "strict_on_arguments_unfold"] let (resolve_implicits_attr_string : Prims.string) = "FStar.Pervasives.resolve_implicits" let (override_resolve_implicits_handler_lid : FStar_Ident.lident) = diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml index fabd224a9fc..0492fdac58c 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml @@ -2220,299 +2220,322 @@ and (encode_term : let uu___7 = FStar_Syntax_Subst.compress head1 in uu___7.FStar_Syntax_Syntax.n in (uu___6, args_e1) in - (match uu___5 with - | uu___6 when is_arithmetic_primitive head1 args_e1 -> - encode_arith_term env head1 args_e1 - | uu___6 when is_BitVector_primitive head1 args_e1 -> - encode_BitVector_term env head1 args_e1 - | (FStar_Syntax_Syntax.Tm_fvar fv, (arg, uu___6)::[]) - when - ((FStar_Syntax_Syntax.fv_eq_lid fv - FStar_Parser_Const.squash_lid) - || - (FStar_Syntax_Syntax.fv_eq_lid fv - FStar_Parser_Const.auto_squash_lid)) - && - (let uu___7 = - FStar_Syntax_Util.destruct_typ_as_formula arg in - FStar_Compiler_Option.isSome uu___7) - -> - let dummy = - FStar_Syntax_Syntax.new_bv - FStar_Pervasives_Native.None - FStar_Syntax_Syntax.t_unit in - let t2 = FStar_Syntax_Util.refine dummy arg in - encode_term t2 env - | (FStar_Syntax_Syntax.Tm_uinst - ({ - FStar_Syntax_Syntax.n = - FStar_Syntax_Syntax.Tm_fvar fv; - FStar_Syntax_Syntax.pos = uu___6; - FStar_Syntax_Syntax.vars = uu___7; - FStar_Syntax_Syntax.hash_code = uu___8;_}, - uu___9), - (arg, uu___10)::[]) when - ((FStar_Syntax_Syntax.fv_eq_lid fv - FStar_Parser_Const.squash_lid) - || - (FStar_Syntax_Syntax.fv_eq_lid fv - FStar_Parser_Const.auto_squash_lid)) - && - (let uu___11 = - FStar_Syntax_Util.destruct_typ_as_formula arg in - FStar_Compiler_Option.isSome uu___11) - -> - let dummy = - FStar_Syntax_Syntax.new_bv - FStar_Pervasives_Native.None - FStar_Syntax_Syntax.t_unit in - let t2 = FStar_Syntax_Util.refine dummy arg in - encode_term t2 env - | (FStar_Syntax_Syntax.Tm_fvar fv, uu___6) when - (Prims.op_Negation - env.FStar_SMTEncoding_Env.encoding_quantifier) - && - ((FStar_Syntax_Syntax.fv_eq_lid fv - FStar_Parser_Const.forall_lid) - || - (FStar_Syntax_Syntax.fv_eq_lid fv - FStar_Parser_Const.exists_lid)) - -> encode_deeply_embedded_quantifier t0 env - | (FStar_Syntax_Syntax.Tm_uinst - ({ - FStar_Syntax_Syntax.n = - FStar_Syntax_Syntax.Tm_fvar fv; - FStar_Syntax_Syntax.pos = uu___6; - FStar_Syntax_Syntax.vars = uu___7; - FStar_Syntax_Syntax.hash_code = uu___8;_}, - uu___9), - uu___10) when - (Prims.op_Negation - env.FStar_SMTEncoding_Env.encoding_quantifier) - && - ((FStar_Syntax_Syntax.fv_eq_lid fv - FStar_Parser_Const.forall_lid) - || - (FStar_Syntax_Syntax.fv_eq_lid fv - FStar_Parser_Const.exists_lid)) - -> encode_deeply_embedded_quantifier t0 env - | (FStar_Syntax_Syntax.Tm_constant - (FStar_Const.Const_range_of), (arg, uu___6)::[]) -> - encode_const - (FStar_Const.Const_range - (arg.FStar_Syntax_Syntax.pos)) env - | (FStar_Syntax_Syntax.Tm_constant - (FStar_Const.Const_set_range_of), - (arg, uu___6)::(rng, uu___7)::[]) -> - encode_term arg env - | (FStar_Syntax_Syntax.Tm_constant - (FStar_Const.Const_reify lopt), uu___6) -> - let fallback uu___7 = - let f = - FStar_SMTEncoding_Env.varops.FStar_SMTEncoding_Env.fresh - env.FStar_SMTEncoding_Env.current_module_name - "Tm_reify" in - let decl = - FStar_SMTEncoding_Term.DeclFun - (f, [], FStar_SMTEncoding_Term.Term_sort, - (FStar_Pervasives_Native.Some - "Imprecise reify")) in - let uu___8 = - let uu___9 = - FStar_SMTEncoding_Term.mk_fv - (f, FStar_SMTEncoding_Term.Term_sort) in - FStar_Compiler_Effect.op_Less_Bar - FStar_SMTEncoding_Util.mkFreeV uu___9 in - let uu___9 = - FStar_Compiler_Effect.op_Bar_Greater [decl] - FStar_SMTEncoding_Term.mk_decls_trivial in - (uu___8, uu___9) in - (match lopt with - | FStar_Pervasives_Native.None -> fallback () - | FStar_Pervasives_Native.Some l when - let uu___7 = - FStar_Compiler_Effect.op_Bar_Greater l - (FStar_TypeChecker_Env.norm_eff_name - env.FStar_SMTEncoding_Env.tcenv) in - FStar_Compiler_Effect.op_Bar_Greater uu___7 - (FStar_TypeChecker_Env.is_layered_effect - env.FStar_SMTEncoding_Env.tcenv) - -> fallback () - | uu___7 -> - let e0 = - let uu___8 = - let uu___9 = - let uu___10 = - FStar_Compiler_Effect.op_Bar_Greater - args_e1 FStar_Compiler_List.hd in - FStar_Compiler_Effect.op_Bar_Greater - uu___10 FStar_Pervasives_Native.fst in - FStar_Syntax_Util.mk_reify uu___9 lopt in - FStar_TypeChecker_Util.norm_reify - env.FStar_SMTEncoding_Env.tcenv [] uu___8 in - ((let uu___9 = - FStar_Compiler_Effect.op_Less_Bar - (FStar_TypeChecker_Env.debug + if is_arithmetic_primitive head1 args_e1 + then encode_arith_term env head1 args_e1 + else + if is_BitVector_primitive head1 args_e1 + then encode_BitVector_term env head1 args_e1 + else + (match uu___5 with + | (FStar_Syntax_Syntax.Tm_fvar fv, + (arg, uu___6)::[]) when + ((FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.squash_lid) + || + (FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.auto_squash_lid)) + && + (let uu___7 = + FStar_Syntax_Util.destruct_typ_as_formula + arg in + FStar_Compiler_Option.isSome uu___7) + -> + let dummy = + FStar_Syntax_Syntax.new_bv + FStar_Pervasives_Native.None + FStar_Syntax_Syntax.t_unit in + let t2 = FStar_Syntax_Util.refine dummy arg in + encode_term t2 env + | (FStar_Syntax_Syntax.Tm_uinst + ({ + FStar_Syntax_Syntax.n = + FStar_Syntax_Syntax.Tm_fvar fv; + FStar_Syntax_Syntax.pos = uu___6; + FStar_Syntax_Syntax.vars = uu___7; + FStar_Syntax_Syntax.hash_code = uu___8;_}, + uu___9), + (arg, uu___10)::[]) when + ((FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.squash_lid) + || + (FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.auto_squash_lid)) + && + (let uu___11 = + FStar_Syntax_Util.destruct_typ_as_formula + arg in + FStar_Compiler_Option.isSome uu___11) + -> + let dummy = + FStar_Syntax_Syntax.new_bv + FStar_Pervasives_Native.None + FStar_Syntax_Syntax.t_unit in + let t2 = FStar_Syntax_Util.refine dummy arg in + encode_term t2 env + | (FStar_Syntax_Syntax.Tm_fvar fv, uu___6) when + (Prims.op_Negation + env.FStar_SMTEncoding_Env.encoding_quantifier) + && + ((FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.forall_lid) + || + (FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.exists_lid)) + -> encode_deeply_embedded_quantifier t0 env + | (FStar_Syntax_Syntax.Tm_uinst + ({ + FStar_Syntax_Syntax.n = + FStar_Syntax_Syntax.Tm_fvar fv; + FStar_Syntax_Syntax.pos = uu___6; + FStar_Syntax_Syntax.vars = uu___7; + FStar_Syntax_Syntax.hash_code = uu___8;_}, + uu___9), + uu___10) when + (Prims.op_Negation + env.FStar_SMTEncoding_Env.encoding_quantifier) + && + ((FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.forall_lid) + || + (FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.exists_lid)) + -> encode_deeply_embedded_quantifier t0 env + | (FStar_Syntax_Syntax.Tm_constant + (FStar_Const.Const_range_of), + (arg, uu___6)::[]) -> + encode_const + (FStar_Const.Const_range + (arg.FStar_Syntax_Syntax.pos)) env + | (FStar_Syntax_Syntax.Tm_constant + (FStar_Const.Const_set_range_of), + (arg, uu___6)::(rng, uu___7)::[]) -> + encode_term arg env + | (FStar_Syntax_Syntax.Tm_constant + (FStar_Const.Const_reify lopt), uu___6) -> + let fallback uu___7 = + let f = + FStar_SMTEncoding_Env.varops.FStar_SMTEncoding_Env.fresh + env.FStar_SMTEncoding_Env.current_module_name + "Tm_reify" in + let decl = + FStar_SMTEncoding_Term.DeclFun + (f, [], + FStar_SMTEncoding_Term.Term_sort, + (FStar_Pervasives_Native.Some + "Imprecise reify")) in + let uu___8 = + let uu___9 = + FStar_SMTEncoding_Term.mk_fv + (f, FStar_SMTEncoding_Term.Term_sort) in + FStar_Compiler_Effect.op_Less_Bar + FStar_SMTEncoding_Util.mkFreeV uu___9 in + let uu___9 = + FStar_Compiler_Effect.op_Bar_Greater + [decl] + FStar_SMTEncoding_Term.mk_decls_trivial in + (uu___8, uu___9) in + (match lopt with + | FStar_Pervasives_Native.None -> fallback () + | FStar_Pervasives_Native.Some l when + let uu___7 = + FStar_Compiler_Effect.op_Bar_Greater l + (FStar_TypeChecker_Env.norm_eff_name + env.FStar_SMTEncoding_Env.tcenv) in + FStar_Compiler_Effect.op_Bar_Greater + uu___7 + (FStar_TypeChecker_Env.is_layered_effect env.FStar_SMTEncoding_Env.tcenv) - (FStar_Options.Other "SMTEncodingReify") in - if uu___9 - then - let uu___10 = - FStar_Syntax_Print.term_to_string e0 in - FStar_Compiler_Util.print1 - "Result of normalization %s\n" uu___10 - else ()); - (let e = - let uu___9 = - FStar_TypeChecker_Util.remove_reify e0 in - let uu___10 = - FStar_Compiler_List.tl args_e1 in - FStar_Syntax_Syntax.mk_Tm_app uu___9 - uu___10 t0.FStar_Syntax_Syntax.pos in - encode_term e env))) - | (FStar_Syntax_Syntax.Tm_constant - (FStar_Const.Const_reflect uu___6), - (arg, uu___7)::[]) -> encode_term arg env - | (FStar_Syntax_Syntax.Tm_fvar fv, - uu___6::(phi, uu___7)::[]) when - FStar_Syntax_Syntax.fv_eq_lid fv - FStar_Parser_Const.by_tactic_lid - -> encode_term phi env - | (FStar_Syntax_Syntax.Tm_uinst - ({ - FStar_Syntax_Syntax.n = - FStar_Syntax_Syntax.Tm_fvar fv; - FStar_Syntax_Syntax.pos = uu___6; - FStar_Syntax_Syntax.vars = uu___7; - FStar_Syntax_Syntax.hash_code = uu___8;_}, - uu___9), - uu___10::(phi, uu___11)::[]) when - FStar_Syntax_Syntax.fv_eq_lid fv - FStar_Parser_Const.by_tactic_lid - -> encode_term phi env - | (FStar_Syntax_Syntax.Tm_fvar fv, - uu___6::uu___7::(phi, uu___8)::[]) when - FStar_Syntax_Syntax.fv_eq_lid fv - FStar_Parser_Const.rewrite_by_tactic_lid - -> encode_term phi env - | (FStar_Syntax_Syntax.Tm_uinst - ({ - FStar_Syntax_Syntax.n = - FStar_Syntax_Syntax.Tm_fvar fv; - FStar_Syntax_Syntax.pos = uu___6; - FStar_Syntax_Syntax.vars = uu___7; - FStar_Syntax_Syntax.hash_code = uu___8;_}, - uu___9), - uu___10::uu___11::(phi, uu___12)::[]) when - FStar_Syntax_Syntax.fv_eq_lid fv - FStar_Parser_Const.rewrite_by_tactic_lid - -> encode_term phi env - | uu___6 -> - let uu___7 = encode_args args_e1 env in - (match uu___7 with - | (args, decls) -> - let encode_partial_app ht_opt = - let uu___8 = encode_term head1 env in - match uu___8 with - | (smt_head, decls') -> - let app_tm = - mk_Apply_args smt_head args in - (match ht_opt with - | uu___9 when - Prims.int_one = Prims.int_one -> - (app_tm, - (FStar_Compiler_List.op_At decls - decls')) - | FStar_Pervasives_Native.Some - (head_type, formals, c) -> - ((let uu___10 = - FStar_TypeChecker_Env.debug - env.FStar_SMTEncoding_Env.tcenv - (FStar_Options.Other - "PartialApp") in - if uu___10 - then - let uu___11 = - FStar_Syntax_Print.term_to_string - head1 in - let uu___12 = - FStar_Syntax_Print.term_to_string - head_type in - let uu___13 = - FStar_Syntax_Print.binders_to_string - ", " formals in - let uu___14 = - FStar_Syntax_Print.comp_to_string - c in - let uu___15 = - FStar_Syntax_Print.args_to_string - args_e1 in - FStar_Compiler_Util.print5 - "Encoding partial application:\n\thead=%s\n\thead_type=%s\n\tformals=%s\n\tcomp=%s\n\tactual args=%s\n" - uu___11 uu___12 uu___13 - uu___14 uu___15 - else ()); - (let uu___10 = - FStar_Compiler_Util.first_N - (FStar_Compiler_List.length - args_e1) formals in - match uu___10 with - | (formals1, rest) -> - let subst = - FStar_Compiler_List.map2 - (fun uu___11 -> - fun uu___12 -> - match (uu___11, - uu___12) - with - | ({ - FStar_Syntax_Syntax.binder_bv - = bv; - FStar_Syntax_Syntax.binder_qual - = uu___13; - FStar_Syntax_Syntax.binder_positivity - = uu___14; - FStar_Syntax_Syntax.binder_attrs - = uu___15;_}, - (a, uu___16)) -> - FStar_Syntax_Syntax.NT - (bv, a)) - formals1 args_e1 in - let ty = - let uu___11 = - FStar_Syntax_Util.arrow - rest c in - FStar_Compiler_Effect.op_Bar_Greater - uu___11 - (FStar_Syntax_Subst.subst - subst) in - ((let uu___12 = + -> fallback () + | uu___7 -> + let e0 = + let uu___8 = + let uu___9 = + let uu___10 = + FStar_Compiler_Effect.op_Bar_Greater + args_e1 FStar_Compiler_List.hd in + FStar_Compiler_Effect.op_Bar_Greater + uu___10 + FStar_Pervasives_Native.fst in + FStar_Syntax_Util.mk_reify uu___9 + lopt in + FStar_TypeChecker_Util.norm_reify + env.FStar_SMTEncoding_Env.tcenv [] + uu___8 in + ((let uu___9 = + FStar_Compiler_Effect.op_Less_Bar + (FStar_TypeChecker_Env.debug + env.FStar_SMTEncoding_Env.tcenv) + (FStar_Options.Other + "SMTEncodingReify") in + if uu___9 + then + let uu___10 = + FStar_Syntax_Print.term_to_string + e0 in + FStar_Compiler_Util.print1 + "Result of normalization %s\n" + uu___10 + else ()); + (let e = + let uu___9 = + FStar_TypeChecker_Util.remove_reify + e0 in + let uu___10 = + FStar_Compiler_List.tl args_e1 in + FStar_Syntax_Syntax.mk_Tm_app uu___9 + uu___10 t0.FStar_Syntax_Syntax.pos in + encode_term e env))) + | (FStar_Syntax_Syntax.Tm_constant + (FStar_Const.Const_reflect uu___6), + (arg, uu___7)::[]) -> encode_term arg env + | (FStar_Syntax_Syntax.Tm_fvar fv, + uu___6::(phi, uu___7)::[]) when + FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.by_tactic_lid + -> encode_term phi env + | (FStar_Syntax_Syntax.Tm_uinst + ({ + FStar_Syntax_Syntax.n = + FStar_Syntax_Syntax.Tm_fvar fv; + FStar_Syntax_Syntax.pos = uu___6; + FStar_Syntax_Syntax.vars = uu___7; + FStar_Syntax_Syntax.hash_code = uu___8;_}, + uu___9), + uu___10::(phi, uu___11)::[]) when + FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.by_tactic_lid + -> encode_term phi env + | (FStar_Syntax_Syntax.Tm_fvar fv, + uu___6::uu___7::(phi, uu___8)::[]) when + FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.rewrite_by_tactic_lid + -> encode_term phi env + | (FStar_Syntax_Syntax.Tm_uinst + ({ + FStar_Syntax_Syntax.n = + FStar_Syntax_Syntax.Tm_fvar fv; + FStar_Syntax_Syntax.pos = uu___6; + FStar_Syntax_Syntax.vars = uu___7; + FStar_Syntax_Syntax.hash_code = uu___8;_}, + uu___9), + uu___10::uu___11::(phi, uu___12)::[]) when + FStar_Syntax_Syntax.fv_eq_lid fv + FStar_Parser_Const.rewrite_by_tactic_lid + -> encode_term phi env + | uu___6 -> + let uu___7 = encode_args args_e1 env in + (match uu___7 with + | (args, decls) -> + let encode_partial_app ht_opt = + let uu___8 = encode_term head1 env in + match uu___8 with + | (smt_head, decls') -> + let app_tm = + mk_Apply_args smt_head args in + if Prims.int_one = Prims.int_one + then + (app_tm, + (FStar_Compiler_List.op_At + decls decls')) + else + (match ht_opt with + | FStar_Pervasives_Native.Some + (head_type, formals, c) -> + ((let uu___10 = FStar_TypeChecker_Env.debug env.FStar_SMTEncoding_Env.tcenv (FStar_Options.Other "PartialApp") in - if uu___12 + if uu___10 then - let uu___13 = + let uu___11 = FStar_Syntax_Print.term_to_string - ty in - FStar_Compiler_Util.print1 - "Encoding partial application, after subst:\n\tty=%s\n" - uu___13 - else ()); - (let uu___12 = + head1 in + let uu___12 = + FStar_Syntax_Print.term_to_string + head_type in let uu___13 = - FStar_Compiler_List.fold_left2 - (fun uu___14 -> - fun uu___15 -> - fun e -> + FStar_Syntax_Print.binders_to_string + ", " formals in + let uu___14 = + FStar_Syntax_Print.comp_to_string + c in + let uu___15 = + FStar_Syntax_Print.args_to_string + args_e1 in + FStar_Compiler_Util.print5 + "Encoding partial application:\n\thead=%s\n\thead_type=%s\n\tformals=%s\n\tcomp=%s\n\tactual args=%s\n" + uu___11 uu___12 + uu___13 uu___14 + uu___15 + else ()); + (let uu___10 = + FStar_Compiler_Util.first_N + (FStar_Compiler_List.length + args_e1) formals in + match uu___10 with + | (formals1, rest) -> + let subst = + FStar_Compiler_List.map2 + (fun uu___11 -> + fun uu___12 -> match - (uu___14, - uu___15) + (uu___11, + uu___12) with - | ((t_hyps, + | ({ + FStar_Syntax_Syntax.binder_bv + = bv; + FStar_Syntax_Syntax.binder_qual + = uu___13; + FStar_Syntax_Syntax.binder_positivity + = uu___14; + FStar_Syntax_Syntax.binder_attrs + = uu___15;_}, + (a, + uu___16)) + -> + FStar_Syntax_Syntax.NT + (bv, a)) + formals1 args_e1 in + let ty = + let uu___11 = + FStar_Syntax_Util.arrow + rest c in + FStar_Compiler_Effect.op_Bar_Greater + uu___11 + (FStar_Syntax_Subst.subst + subst) in + ((let uu___12 = + FStar_TypeChecker_Env.debug + env.FStar_SMTEncoding_Env.tcenv + (FStar_Options.Other + "PartialApp") in + if uu___12 + then + let uu___13 = + FStar_Syntax_Print.term_to_string + ty in + FStar_Compiler_Util.print1 + "Encoding partial application, after subst:\n\tty=%s\n" + uu___13 + else ()); + (let uu___12 = + let uu___13 = + FStar_Compiler_List.fold_left2 + (fun uu___14 + -> + fun uu___15 + -> + fun e -> + match + (uu___14, + uu___15) + with + | + ((t_hyps, decls1), - { + { FStar_Syntax_Syntax.binder_bv = bv; FStar_Syntax_Syntax.binder_qual @@ -2566,53 +2589,63 @@ and (encode_term : (FStar_Compiler_List.op_At decls1 decls'1))))) - ([], []) formals1 - args in - match uu___13 with - | (t_hyps, decls1) -> - let uu___14 = - match smt_head.FStar_SMTEncoding_Term.tm - with - | FStar_SMTEncoding_Term.FreeV - uu___15 -> - encode_term_pred - FStar_Pervasives_Native.None - head_type - env smt_head - | uu___15 -> - (FStar_SMTEncoding_Util.mkTrue, - []) in - (match uu___14 with - | (t_head_hyp, - decls'1) -> - let hyp = - FStar_SMTEncoding_Term.mk_and_l - (t_head_hyp - :: t_hyps) - FStar_Compiler_Range_Type.dummyRange in - let uu___15 = - encode_term_pred - FStar_Pervasives_Native.None - ty env - app_tm in - (match uu___15 - with - | (has_type_conclusion, - decls'') -> - let has_type + ([], []) + formals1 args in + match uu___13 with + | (t_hyps, decls1) + -> + let uu___14 = + match + smt_head.FStar_SMTEncoding_Term.tm + with + | FStar_SMTEncoding_Term.FreeV + uu___15 + -> + encode_term_pred + FStar_Pervasives_Native.None + head_type + env + smt_head + | uu___15 -> + (FStar_SMTEncoding_Util.mkTrue, + []) in + (match uu___14 + with + | (t_head_hyp, + decls'1) + -> + let hyp = + FStar_SMTEncoding_Term.mk_and_l + (t_head_hyp + :: + t_hyps) + FStar_Compiler_Range_Type.dummyRange in + let uu___15 + = + encode_term_pred + FStar_Pervasives_Native.None + ty env + app_tm in + (match uu___15 + with + | + (has_type_conclusion, + decls'') + -> + let has_type = FStar_SMTEncoding_Util.mkImp (hyp, has_type_conclusion) in - let cvars + let cvars = FStar_SMTEncoding_Term.free_variables has_type in - let app_tm_vars + let app_tm_vars = FStar_SMTEncoding_Term.free_variables app_tm in - let uu___16 + let uu___16 = let uu___17 = @@ -2659,7 +2692,7 @@ and (encode_term : uu___22); ([], cvars))) in - (match uu___16 + (match uu___16 with | (pattern1, @@ -2672,275 +2705,301 @@ and (encode_term : (FStar_Compiler_List.op_At decls'1 decls'')))))) in - match uu___12 with - | (vars, pattern1, - has_type, decls'') -> - ((let uu___14 = - FStar_TypeChecker_Env.debug - env.FStar_SMTEncoding_Env.tcenv - (FStar_Options.Other - "PartialApp") in - if uu___14 - then - let uu___15 = - FStar_SMTEncoding_Term.print_smt_term - has_type in - FStar_Compiler_Util.print1 - "Encoding partial application, after SMT encoded predicate:\n\t=%s\n" - uu___15 - else ()); - (let tkey_hash = - FStar_SMTEncoding_Term.hash_of_term - app_tm in - let e_typing = - let uu___14 = - let uu___15 = - FStar_SMTEncoding_Term.mkForall - t0.FStar_Syntax_Syntax.pos - ([pattern1], - vars, - has_type) in - let uu___16 = - let uu___17 = - let uu___18 + match uu___12 with + | (vars, pattern1, + has_type, + decls'') -> + ((let uu___14 = + FStar_TypeChecker_Env.debug + env.FStar_SMTEncoding_Env.tcenv + (FStar_Options.Other + "PartialApp") in + if uu___14 + then + let uu___15 = - FStar_SMTEncoding_Term.hash_of_term + FStar_SMTEncoding_Term.print_smt_term + has_type in + FStar_Compiler_Util.print1 + "Encoding partial application, after SMT encoded predicate:\n\t=%s\n" + uu___15 + else ()); + (let tkey_hash + = + FStar_SMTEncoding_Term.hash_of_term + app_tm in + let e_typing = + let uu___14 + = + let uu___15 + = + FStar_SMTEncoding_Term.mkForall + t0.FStar_Syntax_Syntax.pos + ([pattern1], + vars, + has_type) in + let uu___16 + = + let uu___17 + = + let uu___18 + = + FStar_SMTEncoding_Term.hash_of_term app_tm in - FStar_Compiler_Util.digest_of_string - uu___18 in - Prims.op_Hat - "partial_app_typing_" - uu___17 in - (uu___15, - (FStar_Pervasives_Native.Some - "Partial app typing"), - uu___16) in - FStar_SMTEncoding_Util.mkAssume - uu___14 in - let uu___14 = - let uu___15 = - let uu___16 = - let uu___17 = - FStar_SMTEncoding_Term.mk_decls - "" - tkey_hash - [e_typing] - (FStar_Compiler_List.op_At + FStar_Compiler_Util.digest_of_string + uu___18 in + Prims.op_Hat + "partial_app_typing_" + uu___17 in + (uu___15, + (FStar_Pervasives_Native.Some + "Partial app typing"), + uu___16) in + FStar_SMTEncoding_Util.mkAssume + uu___14 in + let uu___14 = + let uu___15 + = + let uu___16 + = + let uu___17 + = + FStar_SMTEncoding_Term.mk_decls + "" + tkey_hash + [e_typing] + (FStar_Compiler_List.op_At decls (FStar_Compiler_List.op_At decls' decls'')) in - FStar_Compiler_List.op_At - decls'' - uu___17 in - FStar_Compiler_List.op_At - decls' uu___16 in - FStar_Compiler_List.op_At - decls uu___15 in - (app_tm, uu___14))))))) - | FStar_Pervasives_Native.None -> - failwith "impossible") in - let encode_full_app fv = - let uu___8 = - FStar_SMTEncoding_Env.lookup_free_var_sym - env fv in - match uu___8 with - | (fname, fuel_args, arity) -> - let tm = - maybe_curry_app - t0.FStar_Syntax_Syntax.pos fname - arity - (FStar_Compiler_List.op_At - fuel_args args) in - (tm, decls) in - let head2 = FStar_Syntax_Subst.compress head1 in - let head_type = - match head2.FStar_Syntax_Syntax.n with - | FStar_Syntax_Syntax.Tm_uinst - ({ - FStar_Syntax_Syntax.n = - FStar_Syntax_Syntax.Tm_name x; - FStar_Syntax_Syntax.pos = uu___8; - FStar_Syntax_Syntax.vars = uu___9; - FStar_Syntax_Syntax.hash_code = - uu___10;_}, - uu___11) - -> - FStar_Pervasives_Native.Some - (x.FStar_Syntax_Syntax.sort) - | FStar_Syntax_Syntax.Tm_name x -> - FStar_Pervasives_Native.Some - (x.FStar_Syntax_Syntax.sort) - | FStar_Syntax_Syntax.Tm_uinst - ({ - FStar_Syntax_Syntax.n = - FStar_Syntax_Syntax.Tm_fvar fv; - FStar_Syntax_Syntax.pos = uu___8; - FStar_Syntax_Syntax.vars = uu___9; - FStar_Syntax_Syntax.hash_code = - uu___10;_}, - uu___11) - -> - let uu___12 = - let uu___13 = - let uu___14 = - FStar_TypeChecker_Env.lookup_lid - env.FStar_SMTEncoding_Env.tcenv - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in - FStar_Compiler_Effect.op_Bar_Greater - uu___14 - FStar_Pervasives_Native.fst in - FStar_Compiler_Effect.op_Bar_Greater - uu___13 FStar_Pervasives_Native.snd in - FStar_Pervasives_Native.Some uu___12 - | FStar_Syntax_Syntax.Tm_fvar fv -> + FStar_Compiler_List.op_At + decls'' + uu___17 in + FStar_Compiler_List.op_At + decls' + uu___16 in + FStar_Compiler_List.op_At + decls + uu___15 in + (app_tm, + uu___14))))))) + | FStar_Pervasives_Native.None + -> failwith "impossible") in + let encode_full_app fv = let uu___8 = - let uu___9 = - let uu___10 = - FStar_TypeChecker_Env.lookup_lid - env.FStar_SMTEncoding_Env.tcenv - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in - FStar_Compiler_Effect.op_Bar_Greater - uu___10 - FStar_Pervasives_Native.fst in - FStar_Compiler_Effect.op_Bar_Greater - uu___9 FStar_Pervasives_Native.snd in - FStar_Pervasives_Native.Some uu___8 - | FStar_Syntax_Syntax.Tm_ascribed - { FStar_Syntax_Syntax.tm = uu___8; - FStar_Syntax_Syntax.asc = - (FStar_Pervasives.Inl t2, uu___9, - uu___10); - FStar_Syntax_Syntax.eff_opt = uu___11;_} - -> FStar_Pervasives_Native.Some t2 - | FStar_Syntax_Syntax.Tm_ascribed - { FStar_Syntax_Syntax.tm = uu___8; - FStar_Syntax_Syntax.asc = - (FStar_Pervasives.Inr c, uu___9, - uu___10); - FStar_Syntax_Syntax.eff_opt = uu___11;_} - -> - FStar_Pervasives_Native.Some - (FStar_Syntax_Util.comp_result c) - | uu___8 -> FStar_Pervasives_Native.None in - (match head_type with - | FStar_Pervasives_Native.None -> - encode_partial_app - FStar_Pervasives_Native.None - | FStar_Pervasives_Native.Some head_type1 -> - let uu___8 = - let head_type2 = - let uu___9 = - normalize_refinement - [FStar_TypeChecker_Env.Weak; - FStar_TypeChecker_Env.HNF; - FStar_TypeChecker_Env.EraseUniverses] - env.FStar_SMTEncoding_Env.tcenv - head_type1 in - FStar_Compiler_Effect.op_Less_Bar - FStar_Syntax_Util.unrefine uu___9 in - let uu___9 = - curried_arrow_formals_comp - head_type2 in - match uu___9 with - | (formals, c) -> - if - (FStar_Compiler_List.length - formals) - < - (FStar_Compiler_List.length - args) - then - let head_type3 = - let uu___10 = - normalize_refinement - [FStar_TypeChecker_Env.Weak; - FStar_TypeChecker_Env.HNF; - FStar_TypeChecker_Env.EraseUniverses; - FStar_TypeChecker_Env.UnfoldUntil - FStar_Syntax_Syntax.delta_constant] - env.FStar_SMTEncoding_Env.tcenv - head_type2 in - FStar_Compiler_Effect.op_Less_Bar - FStar_Syntax_Util.unrefine - uu___10 in - let uu___10 = - curried_arrow_formals_comp - head_type3 in - (match uu___10 with - | (formals1, c1) -> - (head_type3, formals1, c1)) - else (head_type2, formals, c) in - (match uu___8 with - | (head_type2, formals, c) -> - ((let uu___10 = - FStar_TypeChecker_Env.debug - env.FStar_SMTEncoding_Env.tcenv - (FStar_Options.Other - "PartialApp") in - if uu___10 - then - let uu___11 = - FStar_Syntax_Print.term_to_string - head_type2 in - let uu___12 = - FStar_Syntax_Print.binders_to_string - ", " formals in - let uu___13 = - FStar_Syntax_Print.args_to_string - args_e1 in - FStar_Compiler_Util.print3 - "Encoding partial application, head_type = %s, formals = %s, args = %s\n" - uu___11 uu___12 uu___13 - else ()); - (match head2.FStar_Syntax_Syntax.n - with - | FStar_Syntax_Syntax.Tm_uinst - ({ - FStar_Syntax_Syntax.n = - FStar_Syntax_Syntax.Tm_fvar - fv; - FStar_Syntax_Syntax.pos = - uu___10; - FStar_Syntax_Syntax.vars = - uu___11; - FStar_Syntax_Syntax.hash_code - = uu___12;_}, - uu___13) - when - (FStar_Compiler_List.length - formals) - = - (FStar_Compiler_List.length - args) - -> - encode_full_app - fv.FStar_Syntax_Syntax.fv_name - | FStar_Syntax_Syntax.Tm_fvar fv - when - (FStar_Compiler_List.length - formals) - = - (FStar_Compiler_List.length - args) - -> - encode_full_app - fv.FStar_Syntax_Syntax.fv_name - | uu___10 -> - if - (FStar_Compiler_List.length - formals) - > - (FStar_Compiler_List.length - args) + FStar_SMTEncoding_Env.lookup_free_var_sym + env fv in + match uu___8 with + | (fname, fuel_args, arity) -> + let tm = + maybe_curry_app + t0.FStar_Syntax_Syntax.pos + fname arity + (FStar_Compiler_List.op_At + fuel_args args) in + (tm, decls) in + let head2 = + FStar_Syntax_Subst.compress head1 in + let head_type = + match head2.FStar_Syntax_Syntax.n with + | FStar_Syntax_Syntax.Tm_uinst + ({ + FStar_Syntax_Syntax.n = + FStar_Syntax_Syntax.Tm_name x; + FStar_Syntax_Syntax.pos = uu___8; + FStar_Syntax_Syntax.vars = + uu___9; + FStar_Syntax_Syntax.hash_code = + uu___10;_}, + uu___11) + -> + FStar_Pervasives_Native.Some + (x.FStar_Syntax_Syntax.sort) + | FStar_Syntax_Syntax.Tm_name x -> + FStar_Pervasives_Native.Some + (x.FStar_Syntax_Syntax.sort) + | FStar_Syntax_Syntax.Tm_uinst + ({ + FStar_Syntax_Syntax.n = + FStar_Syntax_Syntax.Tm_fvar fv; + FStar_Syntax_Syntax.pos = uu___8; + FStar_Syntax_Syntax.vars = + uu___9; + FStar_Syntax_Syntax.hash_code = + uu___10;_}, + uu___11) + -> + let uu___12 = + let uu___13 = + let uu___14 = + FStar_TypeChecker_Env.lookup_lid + env.FStar_SMTEncoding_Env.tcenv + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in + FStar_Compiler_Effect.op_Bar_Greater + uu___14 + FStar_Pervasives_Native.fst in + FStar_Compiler_Effect.op_Bar_Greater + uu___13 + FStar_Pervasives_Native.snd in + FStar_Pervasives_Native.Some + uu___12 + | FStar_Syntax_Syntax.Tm_fvar fv -> + let uu___8 = + let uu___9 = + let uu___10 = + FStar_TypeChecker_Env.lookup_lid + env.FStar_SMTEncoding_Env.tcenv + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in + FStar_Compiler_Effect.op_Bar_Greater + uu___10 + FStar_Pervasives_Native.fst in + FStar_Compiler_Effect.op_Bar_Greater + uu___9 + FStar_Pervasives_Native.snd in + FStar_Pervasives_Native.Some uu___8 + | FStar_Syntax_Syntax.Tm_ascribed + { FStar_Syntax_Syntax.tm = uu___8; + FStar_Syntax_Syntax.asc = + (FStar_Pervasives.Inl t2, + uu___9, uu___10); + FStar_Syntax_Syntax.eff_opt = + uu___11;_} + -> FStar_Pervasives_Native.Some t2 + | FStar_Syntax_Syntax.Tm_ascribed + { FStar_Syntax_Syntax.tm = uu___8; + FStar_Syntax_Syntax.asc = + (FStar_Pervasives.Inr c, + uu___9, uu___10); + FStar_Syntax_Syntax.eff_opt = + uu___11;_} + -> + FStar_Pervasives_Native.Some + (FStar_Syntax_Util.comp_result c) + | uu___8 -> + FStar_Pervasives_Native.None in + (match head_type with + | FStar_Pervasives_Native.None -> + encode_partial_app + FStar_Pervasives_Native.None + | FStar_Pervasives_Native.Some + head_type1 -> + let uu___8 = + let head_type2 = + let uu___9 = + normalize_refinement + [FStar_TypeChecker_Env.Weak; + FStar_TypeChecker_Env.HNF; + FStar_TypeChecker_Env.EraseUniverses] + env.FStar_SMTEncoding_Env.tcenv + head_type1 in + FStar_Compiler_Effect.op_Less_Bar + FStar_Syntax_Util.unrefine + uu___9 in + let uu___9 = + curried_arrow_formals_comp + head_type2 in + match uu___9 with + | (formals, c) -> + if + (FStar_Compiler_List.length + formals) + < + (FStar_Compiler_List.length + args) + then + let head_type3 = + let uu___10 = + normalize_refinement + [FStar_TypeChecker_Env.Weak; + FStar_TypeChecker_Env.HNF; + FStar_TypeChecker_Env.EraseUniverses; + FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant] + env.FStar_SMTEncoding_Env.tcenv + head_type2 in + FStar_Compiler_Effect.op_Less_Bar + FStar_Syntax_Util.unrefine + uu___10 in + let uu___10 = + curried_arrow_formals_comp + head_type3 in + (match uu___10 with + | (formals1, c1) -> + (head_type3, formals1, + c1)) + else (head_type2, formals, c) in + (match uu___8 with + | (head_type2, formals, c) -> + ((let uu___10 = + FStar_TypeChecker_Env.debug + env.FStar_SMTEncoding_Env.tcenv + (FStar_Options.Other + "PartialApp") in + if uu___10 then - encode_partial_app - (FStar_Pervasives_Native.Some - (head_type2, formals, - c)) - else - encode_partial_app - FStar_Pervasives_Native.None)))))))) + let uu___11 = + FStar_Syntax_Print.term_to_string + head_type2 in + let uu___12 = + FStar_Syntax_Print.binders_to_string + ", " formals in + let uu___13 = + FStar_Syntax_Print.args_to_string + args_e1 in + FStar_Compiler_Util.print3 + "Encoding partial application, head_type = %s, formals = %s, args = %s\n" + uu___11 uu___12 uu___13 + else ()); + (match head2.FStar_Syntax_Syntax.n + with + | FStar_Syntax_Syntax.Tm_uinst + ({ + FStar_Syntax_Syntax.n + = + FStar_Syntax_Syntax.Tm_fvar + fv; + FStar_Syntax_Syntax.pos + = uu___10; + FStar_Syntax_Syntax.vars + = uu___11; + FStar_Syntax_Syntax.hash_code + = uu___12;_}, + uu___13) + when + (FStar_Compiler_List.length + formals) + = + (FStar_Compiler_List.length + args) + -> + encode_full_app + fv.FStar_Syntax_Syntax.fv_name + | FStar_Syntax_Syntax.Tm_fvar + fv when + (FStar_Compiler_List.length + formals) + = + (FStar_Compiler_List.length + args) + -> + encode_full_app + fv.FStar_Syntax_Syntax.fv_name + | uu___10 -> + if + (FStar_Compiler_List.length + formals) + > + (FStar_Compiler_List.length + args) + then + encode_partial_app + (FStar_Pervasives_Native.Some + (head_type2, + formals, c)) + else + encode_partial_app + FStar_Pervasives_Native.None)))))))) | FStar_Syntax_Syntax.Tm_abs { FStar_Syntax_Syntax.bs = bs; FStar_Syntax_Syntax.body = body; FStar_Syntax_Syntax.rc_opt = lopt;_} diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml index d24fd8c7f16..3a055dba8b0 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml @@ -566,7 +566,7 @@ let (mk_class : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (130)) (Prims.of_int (29)) (Prims.of_int (218)) + (Prims.of_int (130)) (Prims.of_int (29)) (Prims.of_int (224)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> FStar_Reflection_V2_Builtins.explode_qn nm)) @@ -583,7 +583,7 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" (Prims.of_int (132)) (Prims.of_int (4)) - (Prims.of_int (218)) (Prims.of_int (35))))) + (Prims.of_int (224)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -619,7 +619,7 @@ let (mk_class : (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" (Prims.of_int (132)) (Prims.of_int (20)) - (Prims.of_int (218)) (Prims.of_int (35))))) + (Prims.of_int (224)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_Derived.guard (FStar_Pervasives_Native.uu___is_Some r))) @@ -641,7 +641,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (132)) (Prims.of_int (20)) - (Prims.of_int (218)) + (Prims.of_int (224)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> r)) @@ -666,7 +666,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (134)) (Prims.of_int (118)) - (Prims.of_int (218)) + (Prims.of_int (224)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -702,7 +702,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (136)) (Prims.of_int (4)) - (Prims.of_int (218)) + (Prims.of_int (224)) (Prims.of_int (35))))) (Obj.magic ( @@ -728,7 +728,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (136)) (Prims.of_int (29)) - (Prims.of_int (218)) + (Prims.of_int (224)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_Derived.guard @@ -754,7 +754,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (136)) (Prims.of_int (29)) - (Prims.of_int (218)) + (Prims.of_int (224)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -796,7 +796,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (143)) (Prims.of_int (4)) - (Prims.of_int (218)) + (Prims.of_int (224)) (Prims.of_int (35))))) (Obj.magic (last @@ -822,7 +822,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (143)) (Prims.of_int (31)) - (Prims.of_int (218)) + (Prims.of_int (224)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_Derived.guard @@ -849,7 +849,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (143)) (Prims.of_int (31)) - (Prims.of_int (218)) + (Prims.of_int (224)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -881,7 +881,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (144)) (Prims.of_int (33)) - (Prims.of_int (218)) + (Prims.of_int (224)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_SyntaxHelpers.collect_arr_bs @@ -911,7 +911,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (148)) (Prims.of_int (4)) - (Prims.of_int (218)) + (Prims.of_int (224)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -938,7 +938,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (148)) (Prims.of_int (23)) - (Prims.of_int (218)) + (Prims.of_int (224)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_Derived.guard @@ -964,7 +964,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (148)) (Prims.of_int (23)) - (Prims.of_int (218)) + (Prims.of_int (224)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -995,7 +995,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (161)) (Prims.of_int (4)) - (Prims.of_int (218)) + (Prims.of_int (224)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1027,7 +1027,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (162)) (Prims.of_int (45)) - (Prims.of_int (217)) + (Prims.of_int (223)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_V2_Derived.name_of_binder @@ -1051,7 +1051,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (163)) (Prims.of_int (43)) - (Prims.of_int (217)) + (Prims.of_int (223)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_V2_Derived.cur_module @@ -1076,7 +1076,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (164)) (Prims.of_int (49)) - (Prims.of_int (217)) + (Prims.of_int (223)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1105,7 +1105,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (165)) (Prims.of_int (53)) - (Prims.of_int (217)) + (Prims.of_int (223)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_V2_Derived.fresh_namedv_named @@ -1130,7 +1130,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (166)) (Prims.of_int (43)) - (Prims.of_int (217)) + (Prims.of_int (223)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1162,7 +1162,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (173)) (Prims.of_int (22)) - (Prims.of_int (217)) + (Prims.of_int (223)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1227,7 +1227,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (174)) (Prims.of_int (63)) - (Prims.of_int (217)) + (Prims.of_int (223)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1282,7 +1282,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (175)) (Prims.of_int (66)) - (Prims.of_int (217)) + (Prims.of_int (223)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1311,7 +1311,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (184)) (Prims.of_int (20)) - (Prims.of_int (217)) + (Prims.of_int (223)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1450,7 +1450,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (195)) (Prims.of_int (20)) - (Prims.of_int (217)) + (Prims.of_int (223)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1590,7 +1590,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (204)) (Prims.of_int (20)) - (Prims.of_int (217)) + (Prims.of_int (223)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1730,7 +1730,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (208)) (Prims.of_int (39)) - (Prims.of_int (217)) + (Prims.of_int (223)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1756,7 +1756,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (209)) (Prims.of_int (41)) - (Prims.of_int (217)) + (Prims.of_int (223)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1782,7 +1782,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (210)) (Prims.of_int (39)) - (Prims.of_int (217)) + (Prims.of_int (223)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1808,7 +1808,7 @@ let (mk_class : "FStar.Tactics.Typeclasses.fst" (Prims.of_int (212)) (Prims.of_int (87)) - (Prims.of_int (217)) + (Prims.of_int (223)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1842,10 +1842,10 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (215)) + (Prims.of_int (218)) (Prims.of_int (27)) - (Prims.of_int (215)) - (Prims.of_int (54))))) + (Prims.of_int (220)) + (Prims.of_int (56))))) (Obj.magic (FStar_Tactics_NamedView.pack_sigelt (FStar_Tactics_NamedView.Sg_Let @@ -1861,7 +1861,45 @@ let (mk_class : (fun uu___9 -> FStar_Reflection_V2_Builtins.set_sigelt_attrs - b.FStar_Tactics_NamedView.attrs + ((FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_FVar + (FStar_Reflection_V2_Builtins.pack_fv + ["FStar"; + "Pervasives"; + "tcnorm"]))) + :: + (FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_App + ((FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_FVar + (FStar_Reflection_V2_Builtins.pack_fv + ["FStar"; + "Pervasives"; + "strict_on_arguments_unfold"]))), + ((FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_App + ((FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_App + ((FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_FVar + (FStar_Reflection_V2_Builtins.pack_fv + ["Prims"; + "Cons"]))), + ((FStar_Tactics_NamedView.pack + (FStar_Tactics_NamedView.Tv_Const + (FStar_Reflection_V2_Data.C_Int + (FStar_List_Tot_Base.length + params)))), + FStar_Reflection_V2_Data.Q_Explicit)))), + ((FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_FVar + (FStar_Reflection_V2_Builtins.pack_fv + ["Prims"; + "Nil"]))), + FStar_Reflection_V2_Data.Q_Explicit)))), + FStar_Reflection_V2_Data.Q_Explicit)))) + :: + (b.FStar_Tactics_NamedView.attrs)) (FStar_Reflection_V2_Builtins.set_sigelt_quals to_propagate se1))))) diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml index b107db9a02d..bc34fb9e5d9 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml @@ -1978,8 +1978,15 @@ let (cfg_to_string : cfg -> Prims.string) = let uu___1 = let uu___2 = let uu___3 = steps_to_string cfg1.steps in - FStar_Compiler_Util.format1 " steps = %s" uu___3 in - [uu___2; "}"] in + FStar_Compiler_Util.format1 " steps = %s;" uu___3 in + let uu___3 = + let uu___4 = + let uu___5 = + (FStar_Common.string_of_list ()) + FStar_TypeChecker_Env.string_of_delta_level cfg1.delta_level in + FStar_Compiler_Util.format1 " delta_level = %s;" uu___5 in + [uu___4; "}"] in + uu___2 :: uu___3 in "{" :: uu___1 in FStar_String.concat "\n" uu___ let (cfg_env : cfg -> FStar_TypeChecker_Env.env) = fun cfg1 -> cfg1.tcenv diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml index 532ebec7589..8489f91256c 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml @@ -352,7 +352,7 @@ and env = env -> FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term ; strict_args_tab: - Prims.int Prims.list FStar_Pervasives_Native.option + (Prims.bool * Prims.int Prims.list) FStar_Pervasives_Native.option FStar_Compiler_Util.smap ; erasable_types_tab: Prims.bool FStar_Compiler_Util.smap ; @@ -1231,7 +1231,7 @@ let (__proj__Mkenv__item__nbe : unif_allow_ref_guards; erase_erasable_args; core_check;_} -> nbe let (__proj__Mkenv__item__strict_args_tab : env -> - Prims.int Prims.list FStar_Pervasives_Native.option + (Prims.bool * Prims.int Prims.list) FStar_Pervasives_Native.option FStar_Compiler_Util.smap) = fun projectee -> @@ -3833,7 +3833,7 @@ let (fv_has_erasable_attr : env -> FStar_Syntax_Syntax.fv -> Prims.bool) = let (fv_has_strict_args : env -> FStar_Syntax_Syntax.fv -> - Prims.int Prims.list FStar_Pervasives_Native.option) + (Prims.bool * Prims.int Prims.list) FStar_Pervasives_Native.option) = fun env1 -> fun fv -> @@ -3852,7 +3852,27 @@ let (fv_has_strict_args : FStar_ToSyntax_ToSyntax.parse_attr_with_list false x FStar_Parser_Const.strict_on_arguments_attr in FStar_Pervasives_Native.fst uu___1) in - (true, res) in + if FStar_Pervasives_Native.uu___is_Some res + then + (true, + (FStar_Pervasives_Native.Some + (false, + (FStar_Pervasives_Native.__proj__Some__item__v res)))) + else + (let res1 = + FStar_Compiler_Util.find_map attrs1 + (fun x -> + let uu___2 = + FStar_ToSyntax_ToSyntax.parse_attr_with_list false x + FStar_Parser_Const.strict_on_arguments_unfold_attr in + FStar_Pervasives_Native.fst uu___2) in + if FStar_Pervasives_Native.uu___is_Some res1 + then + (true, + (FStar_Pervasives_Native.Some + (true, + (FStar_Pervasives_Native.__proj__Some__item__v res1)))) + else (true, FStar_Pervasives_Native.None)) in cache_in_fv_tab env1.strict_args_tab fv f let (try_lookup_effect_lid : env -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBE.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBE.ml index 160deac13bf..a6cb06d04a4 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBE.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBE.ml @@ -1719,7 +1719,7 @@ and (translate_fv : then FStar_TypeChecker_NBETerm.mkConstruct fvar [] [] else (let uu___2 = - FStar_TypeChecker_Normalize.should_unfold cfg.core_cfg + FStar_TypeChecker_Normalize.should_unfold cfg.core_cfg false (fun uu___3 -> (cfg.core_cfg).FStar_TypeChecker_Cfg.reifying) fvar qninfo in match uu___2 with diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml index be2086791fe..cd867d822d0 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml @@ -232,7 +232,11 @@ let (closure_to_string : closure -> Prims.string) = FStar_Compiler_Util.string_of_int in let uu___4 = FStar_Syntax_Print.term_to_string t in FStar_Compiler_Util.format2 "(env=%s elts; %s)" uu___3 uu___4 - | Univ uu___1 -> "Univ" + | Univ u -> + let uu___1 = + let uu___2 = FStar_Syntax_Print.univ_to_string u in + FStar_String.op_Hat uu___2 ")" in + FStar_String.op_Hat "Univ (" uu___1 | Dummy -> "dummy" let (env_to_string : (FStar_Syntax_Syntax.binder FStar_Pervasives_Native.option * closure) @@ -264,7 +268,11 @@ let (stack_elt_to_string : stack_elt -> Prims.string) = FStar_Compiler_Effect.op_Less_Bar FStar_Compiler_Util.string_of_int (FStar_Compiler_List.length bs) in FStar_Compiler_Util.format1 "Abs %s" uu___5 - | UnivArgs uu___1 -> "UnivArgs" + | UnivArgs (us, uu___1) -> + let uu___2 = + let uu___3 = FStar_Syntax_Print.univs_to_string us in + FStar_String.op_Hat uu___3 ")" in + FStar_String.op_Hat "UnivArgs (" uu___2 | Match uu___1 -> "Match" | App (uu___1, t, uu___2, uu___3) -> let uu___4 = FStar_Syntax_Print.term_to_string t in @@ -352,48 +360,59 @@ let (norm_universe : let u2 = FStar_Syntax_Subst.compress_univ u1 in match u2 with | FStar_Syntax_Syntax.U_bvar x -> - (try - (fun uu___ -> - match () with - | () -> - let uu___1 = - let uu___2 = FStar_Compiler_List.nth env1 x in - FStar_Pervasives_Native.snd uu___2 in - (match uu___1 with - | Univ u3 -> - ((let uu___3 = - FStar_Compiler_Effect.op_Less_Bar - (FStar_TypeChecker_Env.debug - cfg.FStar_TypeChecker_Cfg.tcenv) - (FStar_Options.Other "univ_norm") in - if uu___3 - then - let uu___4 = - FStar_Syntax_Print.univ_to_string u3 in - FStar_Compiler_Util.print1 - "Univ (in norm_universe): %s\n" uu___4 - else ()); - aux u3) - | Dummy -> [u2] - | uu___2 -> - let uu___3 = - let uu___4 = - FStar_Compiler_Util.string_of_int x in - FStar_Compiler_Util.format1 - "Impossible: universe variable u@%s bound to a term" - uu___4 in - failwith uu___3)) () - with - | uu___1 -> + let vo = + try + (fun uu___ -> + match () with + | () -> + let uu___1 = + let uu___2 = FStar_Compiler_List.nth env1 x in + FStar_Pervasives_Native.snd uu___2 in + FStar_Pervasives_Native.Some uu___1) () + with | uu___1 -> FStar_Pervasives_Native.None in + (match vo with + | FStar_Pervasives_Native.Some (Univ u3) -> + ((let uu___1 = + FStar_Compiler_Effect.op_Less_Bar + (FStar_TypeChecker_Env.debug + cfg.FStar_TypeChecker_Cfg.tcenv) + (FStar_Options.Other "univ_norm") in + if uu___1 + then + let uu___2 = FStar_Syntax_Print.univ_to_string u3 in + FStar_Compiler_Util.print1 + "Univ (in norm_universe): %s\n" uu___2 + else ()); + aux u3) + | FStar_Pervasives_Native.Some (Dummy) -> [u2] + | FStar_Pervasives_Native.Some uu___ -> if (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.allow_unbound_universes then [FStar_Syntax_Syntax.U_unknown] else - (let uu___3 = - let uu___4 = FStar_Compiler_Util.string_of_int x in + (let uu___2 = + let uu___3 = FStar_Compiler_Util.string_of_int x in + FStar_Compiler_Util.format1 + "Impossible: universe variable u@%s bound to a term" + uu___3 in + failwith uu___2) + | FStar_Pervasives_Native.None -> + if + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.allow_unbound_universes + then [FStar_Syntax_Syntax.U_unknown] + else + (let uu___1 = + let uu___2 = + let uu___3 = FStar_Compiler_Util.string_of_int x in + let uu___4 = + let uu___5 = + FStar_Compiler_Util.string_of_int + (FStar_Compiler_List.length env1) in + FStar_String.op_Hat " -- " uu___5 in + FStar_String.op_Hat uu___3 uu___4 in FStar_String.op_Hat "Universe variable not found: u@" - uu___4 in - failwith uu___3)) + uu___2 in + failwith uu___1)) | FStar_Syntax_Syntax.U_unif uu___ when (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.check_no_uvars -> [FStar_Syntax_Syntax.U_zero] @@ -1983,896 +2002,946 @@ let (plugin_unfold_warn_ctr : Prims.int FStar_Compiler_Effect.ref) = FStar_Compiler_Util.mk_ref Prims.int_zero let (should_unfold : FStar_TypeChecker_Cfg.cfg -> - (FStar_TypeChecker_Cfg.cfg -> Prims.bool) -> - FStar_Syntax_Syntax.fv -> - FStar_TypeChecker_Env.qninfo -> should_unfold_res) + Prims.bool -> + (FStar_TypeChecker_Cfg.cfg -> Prims.bool) -> + FStar_Syntax_Syntax.fv -> + FStar_TypeChecker_Env.qninfo -> should_unfold_res) = fun cfg -> - fun should_reify1 -> - fun fv -> - fun qninfo -> - let attrs = - let uu___ = FStar_TypeChecker_Env.attrs_of_qninfo qninfo in - match uu___ with - | FStar_Pervasives_Native.None -> [] - | FStar_Pervasives_Native.Some ats -> ats in - let quals = - let uu___ = FStar_TypeChecker_Env.quals_of_qninfo qninfo in - match uu___ with - | FStar_Pervasives_Native.None -> [] - | FStar_Pervasives_Native.Some quals1 -> quals1 in - let yes = (true, false, false) in - let no = (false, false, false) in - let fully = (true, true, false) in - let reif = (true, false, true) in - let yesno b = if b then yes else no in - let fullyno b = if b then fully else no in - let comb_or l = - FStar_Compiler_List.fold_right - (fun uu___ -> - fun uu___1 -> - match (uu___, uu___1) with - | ((a, b, c), (x, y, z)) -> ((a || x), (b || y), (c || z))) - l (false, false, false) in - let string_of_res uu___ = - match uu___ with - | (x, y, z) -> - let uu___1 = FStar_Compiler_Util.string_of_bool x in - let uu___2 = FStar_Compiler_Util.string_of_bool y in - let uu___3 = FStar_Compiler_Util.string_of_bool z in - FStar_Compiler_Util.format3 "(%s,%s,%s)" uu___1 uu___2 uu___3 in - let default_unfolding uu___ = - FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___2 -> - let uu___3 = FStar_Syntax_Print.fv_to_string fv in - let uu___4 = + fun strict_ok -> + fun should_reify1 -> + fun fv -> + fun qninfo -> + let attrs = + let uu___ = FStar_TypeChecker_Env.attrs_of_qninfo qninfo in + match uu___ with + | FStar_Pervasives_Native.None -> [] + | FStar_Pervasives_Native.Some ats -> ats in + let quals = + let uu___ = FStar_TypeChecker_Env.quals_of_qninfo qninfo in + match uu___ with + | FStar_Pervasives_Native.None -> [] + | FStar_Pervasives_Native.Some quals1 -> quals1 in + let yes = (true, false, false) in + let no = (false, false, false) in + let fully = (true, true, false) in + let reif = (true, false, true) in + let yesno b = if b then yes else no in + let fullyno b = if b then fully else no in + let comb_or l = + FStar_Compiler_List.fold_right + (fun uu___ -> + fun uu___1 -> + match (uu___, uu___1) with + | ((a, b, c), (x, y, z)) -> + ((a || x), (b || y), (c || z))) l + (false, false, false) in + let string_of_res uu___ = + match uu___ with + | (x, y, z) -> + let uu___1 = FStar_Compiler_Util.string_of_bool x in + let uu___2 = FStar_Compiler_Util.string_of_bool y in + let uu___3 = FStar_Compiler_Util.string_of_bool z in + FStar_Compiler_Util.format3 "(%s,%s,%s)" uu___1 uu___2 + uu___3 in + let default_unfolding uu___ = + FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___2 -> + let uu___3 = FStar_Syntax_Print.fv_to_string fv in + let uu___4 = + let uu___5 = + FStar_TypeChecker_Env.delta_depth_of_fv + cfg.FStar_TypeChecker_Cfg.tcenv fv in + FStar_Syntax_Print.delta_depth_to_string uu___5 in let uu___5 = - FStar_TypeChecker_Env.delta_depth_of_fv - cfg.FStar_TypeChecker_Cfg.tcenv fv in - FStar_Syntax_Print.delta_depth_to_string uu___5 in - let uu___5 = - (FStar_Common.string_of_list ()) - FStar_TypeChecker_Env.string_of_delta_level - cfg.FStar_TypeChecker_Cfg.delta_level in - FStar_Compiler_Util.print3 - "should_unfold: Reached a %s with delta_depth = %s\n >> Our delta_level is %s\n" - uu___3 uu___4 uu___5); - (let uu___2 = - FStar_Compiler_Effect.op_Bar_Greater - cfg.FStar_TypeChecker_Cfg.delta_level - (FStar_Compiler_Util.for_some - (fun uu___3 -> - match uu___3 with - | FStar_TypeChecker_Env.NoDelta -> false - | FStar_TypeChecker_Env.InliningDelta -> true - | FStar_TypeChecker_Env.Eager_unfolding_only -> true - | FStar_TypeChecker_Env.Unfold l -> - let uu___4 = - FStar_TypeChecker_Env.delta_depth_of_fv - cfg.FStar_TypeChecker_Cfg.tcenv fv in - FStar_TypeChecker_Common.delta_depth_greater_than - uu___4 l)) in - FStar_Compiler_Effect.op_Less_Bar yesno uu___2) in - let res = - if FStar_TypeChecker_Env.qninfo_is_action qninfo - then - let b = should_reify1 cfg in - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___1 -> - let uu___2 = FStar_Syntax_Print.fv_to_string fv in - let uu___3 = FStar_Compiler_Util.string_of_bool b in - FStar_Compiler_Util.print2 - "should_unfold: For DM4F action %s, should_reify = %s\n" - uu___2 uu___3); - if b then reif else no) - else - if - (let uu___ = FStar_TypeChecker_Cfg.find_prim_step cfg fv in - FStar_Compiler_Option.isSome uu___) + (FStar_Common.string_of_list ()) + FStar_TypeChecker_Env.string_of_delta_level + cfg.FStar_TypeChecker_Cfg.delta_level in + FStar_Compiler_Util.print3 + "should_unfold: Reached a %s with delta_depth = %s\n >> Our delta_level is %s\n" + uu___3 uu___4 uu___5); + (let uu___2 = + FStar_Compiler_Effect.op_Bar_Greater + cfg.FStar_TypeChecker_Cfg.delta_level + (FStar_Compiler_Util.for_some + (fun uu___3 -> + match uu___3 with + | FStar_TypeChecker_Env.NoDelta -> false + | FStar_TypeChecker_Env.InliningDelta -> true + | FStar_TypeChecker_Env.Eager_unfolding_only -> true + | FStar_TypeChecker_Env.Unfold l -> + let uu___4 = + FStar_TypeChecker_Env.delta_depth_of_fv + cfg.FStar_TypeChecker_Cfg.tcenv fv in + FStar_TypeChecker_Common.delta_depth_greater_than + uu___4 l)) in + FStar_Compiler_Effect.op_Less_Bar yesno uu___2) in + let res = + if FStar_TypeChecker_Env.qninfo_is_action qninfo then + let b = should_reify1 cfg in (FStar_TypeChecker_Cfg.log_unfolding cfg (fun uu___1 -> - FStar_Compiler_Util.print_string - " >> It's a primop, not unfolding\n"); - no) + let uu___2 = FStar_Syntax_Print.fv_to_string fv in + let uu___3 = FStar_Compiler_Util.string_of_bool b in + FStar_Compiler_Util.print2 + "should_unfold: For DM4F action %s, should_reify = %s\n" + uu___2 uu___3); + if b then reif else no) else - (match (qninfo, - ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only), - ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully), - ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr), - ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual), - ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace)) - with - | (FStar_Pervasives_Native.Some - (FStar_Pervasives.Inr - ({ - FStar_Syntax_Syntax.sigel = - FStar_Syntax_Syntax.Sig_let - { FStar_Syntax_Syntax.lbs1 = (is_rec, uu___); - FStar_Syntax_Syntax.lids1 = uu___1;_}; - FStar_Syntax_Syntax.sigrng = uu___2; - FStar_Syntax_Syntax.sigquals = qs; - FStar_Syntax_Syntax.sigmeta = uu___3; - FStar_Syntax_Syntax.sigattrs = uu___4; - FStar_Syntax_Syntax.sigopens_and_abbrevs = uu___5; - FStar_Syntax_Syntax.sigopts = uu___6;_}, - uu___7), - uu___8), - uu___9, uu___10, uu___11, uu___12, uu___13) when - FStar_Compiler_List.contains - FStar_Syntax_Syntax.HasMaskedEffect qs - -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___15 -> - FStar_Compiler_Util.print_string - " >> HasMaskedEffect, not unfolding\n"); - no) - | (uu___, uu___1, uu___2, uu___3, uu___4, uu___5) when - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_tac - && - (FStar_Compiler_Util.for_some - (FStar_Syntax_Util.attr_eq - FStar_Syntax_Util.tac_opaque_attr) attrs) - -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___7 -> - FStar_Compiler_Util.print_string - " >> tac_opaque, not unfolding\n"); - no) - | (FStar_Pervasives_Native.Some - (FStar_Pervasives.Inr - ({ - FStar_Syntax_Syntax.sigel = - FStar_Syntax_Syntax.Sig_let - { FStar_Syntax_Syntax.lbs1 = (is_rec, uu___); - FStar_Syntax_Syntax.lids1 = uu___1;_}; - FStar_Syntax_Syntax.sigrng = uu___2; - FStar_Syntax_Syntax.sigquals = qs; - FStar_Syntax_Syntax.sigmeta = uu___3; - FStar_Syntax_Syntax.sigattrs = uu___4; - FStar_Syntax_Syntax.sigopens_and_abbrevs = uu___5; - FStar_Syntax_Syntax.sigopts = uu___6;_}, - uu___7), - uu___8), - uu___9, uu___10, uu___11, uu___12, uu___13) when - (is_rec && - (Prims.op_Negation - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.zeta)) - && - (Prims.op_Negation - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.zeta_full) - -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___15 -> - FStar_Compiler_Util.print_string - " >> It's a recursive definition but we're not doing Zeta, not unfolding\n"); - no) - | (uu___, FStar_Pervasives_Native.Some uu___1, uu___2, - uu___3, uu___4, uu___5) -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___7 -> - let uu___8 = FStar_Syntax_Print.fv_to_string fv in - FStar_Compiler_Util.print1 - "should_unfold: Reached a %s with selective unfolding\n" - uu___8); - (let meets_some_criterion = - let uu___7 = - let uu___8 = - if - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction - then + if + (Prims.op_Negation strict_ok) && + ((let uu___ = + FStar_TypeChecker_Env.fv_has_strict_args + cfg.FStar_TypeChecker_Cfg.tcenv fv in + FStar_Pervasives_Native.uu___is_Some uu___)) + then + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___1 -> + FStar_Compiler_Util.print_string + " >> Not unfolding strict_on_arguments definition\n"); + no) + else + if + (let uu___ = FStar_TypeChecker_Cfg.find_prim_step cfg fv in + FStar_Compiler_Option.isSome uu___) + then + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___1 -> + FStar_Compiler_Util.print_string + " >> It's a primop, not unfolding\n"); + no) + else + (match (qninfo, + ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only), + ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully), + ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr), + ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual), + ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace)) + with + | (FStar_Pervasives_Native.Some + (FStar_Pervasives.Inr + ({ + FStar_Syntax_Syntax.sigel = + FStar_Syntax_Syntax.Sig_let + { FStar_Syntax_Syntax.lbs1 = (is_rec, uu___); + FStar_Syntax_Syntax.lids1 = uu___1;_}; + FStar_Syntax_Syntax.sigrng = uu___2; + FStar_Syntax_Syntax.sigquals = qs; + FStar_Syntax_Syntax.sigmeta = uu___3; + FStar_Syntax_Syntax.sigattrs = uu___4; + FStar_Syntax_Syntax.sigopens_and_abbrevs = uu___5; + FStar_Syntax_Syntax.sigopts = uu___6;_}, + uu___7), + uu___8), + uu___9, uu___10, uu___11, uu___12, uu___13) when + FStar_Compiler_List.contains + FStar_Syntax_Syntax.HasMaskedEffect qs + -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___15 -> + FStar_Compiler_Util.print_string + " >> HasMaskedEffect, not unfolding\n"); + no) + | (uu___, uu___1, uu___2, uu___3, uu___4, uu___5) when + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_tac + && + (FStar_Compiler_Util.for_some + (FStar_Syntax_Util.attr_eq + FStar_Syntax_Util.tac_opaque_attr) attrs) + -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___7 -> + FStar_Compiler_Util.print_string + " >> tac_opaque, not unfolding\n"); + no) + | (FStar_Pervasives_Native.Some + (FStar_Pervasives.Inr + ({ + FStar_Syntax_Syntax.sigel = + FStar_Syntax_Syntax.Sig_let + { FStar_Syntax_Syntax.lbs1 = (is_rec, uu___); + FStar_Syntax_Syntax.lids1 = uu___1;_}; + FStar_Syntax_Syntax.sigrng = uu___2; + FStar_Syntax_Syntax.sigquals = qs; + FStar_Syntax_Syntax.sigmeta = uu___3; + FStar_Syntax_Syntax.sigattrs = uu___4; + FStar_Syntax_Syntax.sigopens_and_abbrevs = uu___5; + FStar_Syntax_Syntax.sigopts = uu___6;_}, + uu___7), + uu___8), + uu___9, uu___10, uu___11, uu___12, uu___13) when + (is_rec && + (Prims.op_Negation + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.zeta)) + && + (Prims.op_Negation + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.zeta_full) + -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___15 -> + FStar_Compiler_Util.print_string + " >> It's a recursive definition but we're not doing Zeta, not unfolding\n"); + no) + | (uu___, FStar_Pervasives_Native.Some uu___1, uu___2, + uu___3, uu___4, uu___5) -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___7 -> + let uu___8 = + FStar_Syntax_Print.fv_to_string fv in + FStar_Compiler_Util.print1 + "should_unfold: Reached a %s with selective unfolding\n" + uu___8); + (let meets_some_criterion = + let uu___7 = + let uu___8 = + if + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction + then + let uu___9 = + let uu___10 = + FStar_TypeChecker_Env.lookup_definition_qninfo + [FStar_TypeChecker_Env.Eager_unfolding_only; + FStar_TypeChecker_Env.InliningDelta] + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v + qninfo in + FStar_Compiler_Option.isSome uu___10 in + FStar_Compiler_Effect.op_Less_Bar yesno + uu___9 + else no in let uu___9 = let uu___10 = - FStar_TypeChecker_Env.lookup_definition_qninfo - [FStar_TypeChecker_Env.Eager_unfolding_only; - FStar_TypeChecker_Env.InliningDelta] - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v - qninfo in - FStar_Compiler_Option.isSome uu___10 in - FStar_Compiler_Effect.op_Less_Bar yesno uu___9 - else no in - let uu___9 = - let uu___10 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___11 = - FStar_Compiler_Util.for_some - (FStar_Syntax_Syntax.fv_eq_lid fv) - lids in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___11 in - let uu___11 = - let uu___12 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___13 = - FStar_Compiler_Util.for_some - (fun at -> - FStar_Compiler_Util.for_some - (fun lid -> - FStar_Syntax_Util.is_fvar - lid at) lids) attrs in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___13 in - let uu___13 = - let uu___14 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only with | FStar_Pervasives_Native.None -> no | FStar_Pervasives_Native.Some lids -> - let uu___15 = + let uu___11 = FStar_Compiler_Util.for_some (FStar_Syntax_Syntax.fv_eq_lid fv) lids in FStar_Compiler_Effect.op_Less_Bar - fullyno uu___15 in - let uu___15 = - let uu___16 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + yesno uu___11 in + let uu___11 = + let uu___12 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some qs -> - let uu___17 = + | FStar_Pervasives_Native.Some lids -> + let uu___13 = FStar_Compiler_Util.for_some - (fun q -> + (fun at -> FStar_Compiler_Util.for_some - (fun qual -> - let uu___18 = - FStar_Syntax_Print.qual_to_string - qual in - uu___18 = q) quals) qs in + (fun lid -> + FStar_Syntax_Util.is_fvar + lid at) lids) attrs in FStar_Compiler_Effect.op_Less_Bar - yesno uu___17 in - let uu___17 = - let uu___18 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + yesno uu___13 in + let uu___13 = + let uu___14 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some - namespaces -> - let uu___19 = + | FStar_Pervasives_Native.Some lids -> + let uu___15 = FStar_Compiler_Util.for_some - (fun ns -> - let uu___20 = - let uu___21 = - FStar_Syntax_Syntax.lid_of_fv - fv in - FStar_Ident.nsstr uu___21 in - FStar_Compiler_Util.starts_with - uu___20 ns) namespaces in + (FStar_Syntax_Syntax.fv_eq_lid + fv) lids in FStar_Compiler_Effect.op_Less_Bar - yesno uu___19 in - [uu___18] in - uu___16 :: uu___17 in - uu___14 :: uu___15 in - uu___12 :: uu___13 in - uu___10 :: uu___11 in - uu___8 :: uu___9 in - comb_or uu___7 in - meets_some_criterion)) - | (uu___, uu___1, FStar_Pervasives_Native.Some uu___2, - uu___3, uu___4, uu___5) -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___7 -> - let uu___8 = FStar_Syntax_Print.fv_to_string fv in - FStar_Compiler_Util.print1 - "should_unfold: Reached a %s with selective unfolding\n" - uu___8); - (let meets_some_criterion = - let uu___7 = - let uu___8 = - if - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction - then + fullyno uu___15 in + let uu___15 = + let uu___16 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + with + | FStar_Pervasives_Native.None -> no + | FStar_Pervasives_Native.Some qs -> + let uu___17 = + FStar_Compiler_Util.for_some + (fun q -> + FStar_Compiler_Util.for_some + (fun qual -> + let uu___18 = + FStar_Syntax_Print.qual_to_string + qual in + uu___18 = q) quals) + qs in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___17 in + let uu___17 = + let uu___18 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + with + | FStar_Pervasives_Native.None -> + no + | FStar_Pervasives_Native.Some + namespaces -> + let uu___19 = + FStar_Compiler_Util.for_some + (fun ns -> + let uu___20 = + let uu___21 = + FStar_Syntax_Syntax.lid_of_fv + fv in + FStar_Ident.nsstr + uu___21 in + FStar_Compiler_Util.starts_with + uu___20 ns) + namespaces in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___19 in + [uu___18] in + uu___16 :: uu___17 in + uu___14 :: uu___15 in + uu___12 :: uu___13 in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + comb_or uu___7 in + meets_some_criterion)) + | (uu___, uu___1, FStar_Pervasives_Native.Some uu___2, + uu___3, uu___4, uu___5) -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___7 -> + let uu___8 = + FStar_Syntax_Print.fv_to_string fv in + FStar_Compiler_Util.print1 + "should_unfold: Reached a %s with selective unfolding\n" + uu___8); + (let meets_some_criterion = + let uu___7 = + let uu___8 = + if + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction + then + let uu___9 = + let uu___10 = + FStar_TypeChecker_Env.lookup_definition_qninfo + [FStar_TypeChecker_Env.Eager_unfolding_only; + FStar_TypeChecker_Env.InliningDelta] + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v + qninfo in + FStar_Compiler_Option.isSome uu___10 in + FStar_Compiler_Effect.op_Less_Bar yesno + uu___9 + else no in let uu___9 = let uu___10 = - FStar_TypeChecker_Env.lookup_definition_qninfo - [FStar_TypeChecker_Env.Eager_unfolding_only; - FStar_TypeChecker_Env.InliningDelta] - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v - qninfo in - FStar_Compiler_Option.isSome uu___10 in - FStar_Compiler_Effect.op_Less_Bar yesno uu___9 - else no in - let uu___9 = - let uu___10 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___11 = - FStar_Compiler_Util.for_some - (FStar_Syntax_Syntax.fv_eq_lid fv) - lids in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___11 in - let uu___11 = - let uu___12 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___13 = - FStar_Compiler_Util.for_some - (fun at -> - FStar_Compiler_Util.for_some - (fun lid -> - FStar_Syntax_Util.is_fvar - lid at) lids) attrs in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___13 in - let uu___13 = - let uu___14 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only with | FStar_Pervasives_Native.None -> no | FStar_Pervasives_Native.Some lids -> - let uu___15 = + let uu___11 = FStar_Compiler_Util.for_some (FStar_Syntax_Syntax.fv_eq_lid fv) lids in FStar_Compiler_Effect.op_Less_Bar - fullyno uu___15 in - let uu___15 = - let uu___16 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + yesno uu___11 in + let uu___11 = + let uu___12 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some qs -> - let uu___17 = + | FStar_Pervasives_Native.Some lids -> + let uu___13 = FStar_Compiler_Util.for_some - (fun q -> + (fun at -> FStar_Compiler_Util.for_some - (fun qual -> - let uu___18 = - FStar_Syntax_Print.qual_to_string - qual in - uu___18 = q) quals) qs in + (fun lid -> + FStar_Syntax_Util.is_fvar + lid at) lids) attrs in FStar_Compiler_Effect.op_Less_Bar - yesno uu___17 in - let uu___17 = - let uu___18 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + yesno uu___13 in + let uu___13 = + let uu___14 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some - namespaces -> - let uu___19 = + | FStar_Pervasives_Native.Some lids -> + let uu___15 = FStar_Compiler_Util.for_some - (fun ns -> - let uu___20 = - let uu___21 = - FStar_Syntax_Syntax.lid_of_fv - fv in - FStar_Ident.nsstr uu___21 in - FStar_Compiler_Util.starts_with - uu___20 ns) namespaces in + (FStar_Syntax_Syntax.fv_eq_lid + fv) lids in FStar_Compiler_Effect.op_Less_Bar - yesno uu___19 in - [uu___18] in - uu___16 :: uu___17 in - uu___14 :: uu___15 in - uu___12 :: uu___13 in - uu___10 :: uu___11 in - uu___8 :: uu___9 in - comb_or uu___7 in - meets_some_criterion)) - | (uu___, uu___1, uu___2, FStar_Pervasives_Native.Some - uu___3, uu___4, uu___5) -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___7 -> - let uu___8 = FStar_Syntax_Print.fv_to_string fv in - FStar_Compiler_Util.print1 - "should_unfold: Reached a %s with selective unfolding\n" - uu___8); - (let meets_some_criterion = - let uu___7 = - let uu___8 = - if - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction - then + fullyno uu___15 in + let uu___15 = + let uu___16 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + with + | FStar_Pervasives_Native.None -> no + | FStar_Pervasives_Native.Some qs -> + let uu___17 = + FStar_Compiler_Util.for_some + (fun q -> + FStar_Compiler_Util.for_some + (fun qual -> + let uu___18 = + FStar_Syntax_Print.qual_to_string + qual in + uu___18 = q) quals) + qs in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___17 in + let uu___17 = + let uu___18 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + with + | FStar_Pervasives_Native.None -> + no + | FStar_Pervasives_Native.Some + namespaces -> + let uu___19 = + FStar_Compiler_Util.for_some + (fun ns -> + let uu___20 = + let uu___21 = + FStar_Syntax_Syntax.lid_of_fv + fv in + FStar_Ident.nsstr + uu___21 in + FStar_Compiler_Util.starts_with + uu___20 ns) + namespaces in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___19 in + [uu___18] in + uu___16 :: uu___17 in + uu___14 :: uu___15 in + uu___12 :: uu___13 in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + comb_or uu___7 in + meets_some_criterion)) + | (uu___, uu___1, uu___2, FStar_Pervasives_Native.Some + uu___3, uu___4, uu___5) -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___7 -> + let uu___8 = + FStar_Syntax_Print.fv_to_string fv in + FStar_Compiler_Util.print1 + "should_unfold: Reached a %s with selective unfolding\n" + uu___8); + (let meets_some_criterion = + let uu___7 = + let uu___8 = + if + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction + then + let uu___9 = + let uu___10 = + FStar_TypeChecker_Env.lookup_definition_qninfo + [FStar_TypeChecker_Env.Eager_unfolding_only; + FStar_TypeChecker_Env.InliningDelta] + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v + qninfo in + FStar_Compiler_Option.isSome uu___10 in + FStar_Compiler_Effect.op_Less_Bar yesno + uu___9 + else no in let uu___9 = let uu___10 = - FStar_TypeChecker_Env.lookup_definition_qninfo - [FStar_TypeChecker_Env.Eager_unfolding_only; - FStar_TypeChecker_Env.InliningDelta] - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v - qninfo in - FStar_Compiler_Option.isSome uu___10 in - FStar_Compiler_Effect.op_Less_Bar yesno uu___9 - else no in - let uu___9 = - let uu___10 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___11 = - FStar_Compiler_Util.for_some - (FStar_Syntax_Syntax.fv_eq_lid fv) - lids in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___11 in - let uu___11 = - let uu___12 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___13 = - FStar_Compiler_Util.for_some - (fun at -> - FStar_Compiler_Util.for_some - (fun lid -> - FStar_Syntax_Util.is_fvar - lid at) lids) attrs in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___13 in - let uu___13 = - let uu___14 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only with | FStar_Pervasives_Native.None -> no | FStar_Pervasives_Native.Some lids -> - let uu___15 = + let uu___11 = FStar_Compiler_Util.for_some (FStar_Syntax_Syntax.fv_eq_lid fv) lids in FStar_Compiler_Effect.op_Less_Bar - fullyno uu___15 in - let uu___15 = - let uu___16 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + yesno uu___11 in + let uu___11 = + let uu___12 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some qs -> - let uu___17 = + | FStar_Pervasives_Native.Some lids -> + let uu___13 = FStar_Compiler_Util.for_some - (fun q -> + (fun at -> FStar_Compiler_Util.for_some - (fun qual -> - let uu___18 = - FStar_Syntax_Print.qual_to_string - qual in - uu___18 = q) quals) qs in + (fun lid -> + FStar_Syntax_Util.is_fvar + lid at) lids) attrs in FStar_Compiler_Effect.op_Less_Bar - yesno uu___17 in - let uu___17 = - let uu___18 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + yesno uu___13 in + let uu___13 = + let uu___14 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some - namespaces -> - let uu___19 = + | FStar_Pervasives_Native.Some lids -> + let uu___15 = FStar_Compiler_Util.for_some - (fun ns -> - let uu___20 = - let uu___21 = - FStar_Syntax_Syntax.lid_of_fv - fv in - FStar_Ident.nsstr uu___21 in - FStar_Compiler_Util.starts_with - uu___20 ns) namespaces in + (FStar_Syntax_Syntax.fv_eq_lid + fv) lids in FStar_Compiler_Effect.op_Less_Bar - yesno uu___19 in - [uu___18] in - uu___16 :: uu___17 in - uu___14 :: uu___15 in - uu___12 :: uu___13 in - uu___10 :: uu___11 in - uu___8 :: uu___9 in - comb_or uu___7 in - meets_some_criterion)) - | (uu___, uu___1, uu___2, uu___3, - FStar_Pervasives_Native.Some uu___4, uu___5) -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___7 -> - let uu___8 = FStar_Syntax_Print.fv_to_string fv in - FStar_Compiler_Util.print1 - "should_unfold: Reached a %s with selective unfolding\n" - uu___8); - (let meets_some_criterion = - let uu___7 = - let uu___8 = - if - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction - then + fullyno uu___15 in + let uu___15 = + let uu___16 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + with + | FStar_Pervasives_Native.None -> no + | FStar_Pervasives_Native.Some qs -> + let uu___17 = + FStar_Compiler_Util.for_some + (fun q -> + FStar_Compiler_Util.for_some + (fun qual -> + let uu___18 = + FStar_Syntax_Print.qual_to_string + qual in + uu___18 = q) quals) + qs in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___17 in + let uu___17 = + let uu___18 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + with + | FStar_Pervasives_Native.None -> + no + | FStar_Pervasives_Native.Some + namespaces -> + let uu___19 = + FStar_Compiler_Util.for_some + (fun ns -> + let uu___20 = + let uu___21 = + FStar_Syntax_Syntax.lid_of_fv + fv in + FStar_Ident.nsstr + uu___21 in + FStar_Compiler_Util.starts_with + uu___20 ns) + namespaces in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___19 in + [uu___18] in + uu___16 :: uu___17 in + uu___14 :: uu___15 in + uu___12 :: uu___13 in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + comb_or uu___7 in + meets_some_criterion)) + | (uu___, uu___1, uu___2, uu___3, + FStar_Pervasives_Native.Some uu___4, uu___5) -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___7 -> + let uu___8 = + FStar_Syntax_Print.fv_to_string fv in + FStar_Compiler_Util.print1 + "should_unfold: Reached a %s with selective unfolding\n" + uu___8); + (let meets_some_criterion = + let uu___7 = + let uu___8 = + if + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction + then + let uu___9 = + let uu___10 = + FStar_TypeChecker_Env.lookup_definition_qninfo + [FStar_TypeChecker_Env.Eager_unfolding_only; + FStar_TypeChecker_Env.InliningDelta] + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v + qninfo in + FStar_Compiler_Option.isSome uu___10 in + FStar_Compiler_Effect.op_Less_Bar yesno + uu___9 + else no in let uu___9 = let uu___10 = - FStar_TypeChecker_Env.lookup_definition_qninfo - [FStar_TypeChecker_Env.Eager_unfolding_only; - FStar_TypeChecker_Env.InliningDelta] - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v - qninfo in - FStar_Compiler_Option.isSome uu___10 in - FStar_Compiler_Effect.op_Less_Bar yesno uu___9 - else no in - let uu___9 = - let uu___10 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___11 = - FStar_Compiler_Util.for_some - (FStar_Syntax_Syntax.fv_eq_lid fv) - lids in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___11 in - let uu___11 = - let uu___12 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___13 = - FStar_Compiler_Util.for_some - (fun at -> - FStar_Compiler_Util.for_some - (fun lid -> - FStar_Syntax_Util.is_fvar - lid at) lids) attrs in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___13 in - let uu___13 = - let uu___14 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only with | FStar_Pervasives_Native.None -> no | FStar_Pervasives_Native.Some lids -> - let uu___15 = + let uu___11 = FStar_Compiler_Util.for_some (FStar_Syntax_Syntax.fv_eq_lid fv) lids in FStar_Compiler_Effect.op_Less_Bar - fullyno uu___15 in - let uu___15 = - let uu___16 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + yesno uu___11 in + let uu___11 = + let uu___12 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some qs -> - let uu___17 = + | FStar_Pervasives_Native.Some lids -> + let uu___13 = FStar_Compiler_Util.for_some - (fun q -> + (fun at -> FStar_Compiler_Util.for_some - (fun qual -> - let uu___18 = - FStar_Syntax_Print.qual_to_string - qual in - uu___18 = q) quals) qs in + (fun lid -> + FStar_Syntax_Util.is_fvar + lid at) lids) attrs in FStar_Compiler_Effect.op_Less_Bar - yesno uu___17 in - let uu___17 = - let uu___18 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + yesno uu___13 in + let uu___13 = + let uu___14 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some - namespaces -> - let uu___19 = + | FStar_Pervasives_Native.Some lids -> + let uu___15 = FStar_Compiler_Util.for_some - (fun ns -> - let uu___20 = - let uu___21 = - FStar_Syntax_Syntax.lid_of_fv - fv in - FStar_Ident.nsstr uu___21 in - FStar_Compiler_Util.starts_with - uu___20 ns) namespaces in + (FStar_Syntax_Syntax.fv_eq_lid + fv) lids in FStar_Compiler_Effect.op_Less_Bar - yesno uu___19 in - [uu___18] in - uu___16 :: uu___17 in - uu___14 :: uu___15 in - uu___12 :: uu___13 in - uu___10 :: uu___11 in - uu___8 :: uu___9 in - comb_or uu___7 in - meets_some_criterion)) - | (uu___, uu___1, uu___2, uu___3, uu___4, - FStar_Pervasives_Native.Some uu___5) -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___7 -> - let uu___8 = FStar_Syntax_Print.fv_to_string fv in - FStar_Compiler_Util.print1 - "should_unfold: Reached a %s with selective unfolding\n" - uu___8); - (let meets_some_criterion = - let uu___7 = - let uu___8 = - if - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction - then + fullyno uu___15 in + let uu___15 = + let uu___16 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + with + | FStar_Pervasives_Native.None -> no + | FStar_Pervasives_Native.Some qs -> + let uu___17 = + FStar_Compiler_Util.for_some + (fun q -> + FStar_Compiler_Util.for_some + (fun qual -> + let uu___18 = + FStar_Syntax_Print.qual_to_string + qual in + uu___18 = q) quals) + qs in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___17 in + let uu___17 = + let uu___18 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + with + | FStar_Pervasives_Native.None -> + no + | FStar_Pervasives_Native.Some + namespaces -> + let uu___19 = + FStar_Compiler_Util.for_some + (fun ns -> + let uu___20 = + let uu___21 = + FStar_Syntax_Syntax.lid_of_fv + fv in + FStar_Ident.nsstr + uu___21 in + FStar_Compiler_Util.starts_with + uu___20 ns) + namespaces in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___19 in + [uu___18] in + uu___16 :: uu___17 in + uu___14 :: uu___15 in + uu___12 :: uu___13 in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + comb_or uu___7 in + meets_some_criterion)) + | (uu___, uu___1, uu___2, uu___3, uu___4, + FStar_Pervasives_Native.Some uu___5) -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___7 -> + let uu___8 = + FStar_Syntax_Print.fv_to_string fv in + FStar_Compiler_Util.print1 + "should_unfold: Reached a %s with selective unfolding\n" + uu___8); + (let meets_some_criterion = + let uu___7 = + let uu___8 = + if + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction + then + let uu___9 = + let uu___10 = + FStar_TypeChecker_Env.lookup_definition_qninfo + [FStar_TypeChecker_Env.Eager_unfolding_only; + FStar_TypeChecker_Env.InliningDelta] + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v + qninfo in + FStar_Compiler_Option.isSome uu___10 in + FStar_Compiler_Effect.op_Less_Bar yesno + uu___9 + else no in let uu___9 = let uu___10 = - FStar_TypeChecker_Env.lookup_definition_qninfo - [FStar_TypeChecker_Env.Eager_unfolding_only; - FStar_TypeChecker_Env.InliningDelta] - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v - qninfo in - FStar_Compiler_Option.isSome uu___10 in - FStar_Compiler_Effect.op_Less_Bar yesno uu___9 - else no in - let uu___9 = - let uu___10 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___11 = - FStar_Compiler_Util.for_some - (FStar_Syntax_Syntax.fv_eq_lid fv) - lids in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___11 in - let uu___11 = - let uu___12 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___13 = - FStar_Compiler_Util.for_some - (fun at -> - FStar_Compiler_Util.for_some - (fun lid -> - FStar_Syntax_Util.is_fvar - lid at) lids) attrs in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___13 in - let uu___13 = - let uu___14 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only with | FStar_Pervasives_Native.None -> no | FStar_Pervasives_Native.Some lids -> - let uu___15 = + let uu___11 = FStar_Compiler_Util.for_some (FStar_Syntax_Syntax.fv_eq_lid fv) lids in FStar_Compiler_Effect.op_Less_Bar - fullyno uu___15 in - let uu___15 = - let uu___16 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + yesno uu___11 in + let uu___11 = + let uu___12 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some qs -> - let uu___17 = + | FStar_Pervasives_Native.Some lids -> + let uu___13 = FStar_Compiler_Util.for_some - (fun q -> + (fun at -> FStar_Compiler_Util.for_some - (fun qual -> - let uu___18 = - FStar_Syntax_Print.qual_to_string - qual in - uu___18 = q) quals) qs in + (fun lid -> + FStar_Syntax_Util.is_fvar + lid at) lids) attrs in FStar_Compiler_Effect.op_Less_Bar - yesno uu___17 in - let uu___17 = - let uu___18 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + yesno uu___13 in + let uu___13 = + let uu___14 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some - namespaces -> - let uu___19 = + | FStar_Pervasives_Native.Some lids -> + let uu___15 = FStar_Compiler_Util.for_some - (fun ns -> - let uu___20 = - let uu___21 = - FStar_Syntax_Syntax.lid_of_fv - fv in - FStar_Ident.nsstr uu___21 in - FStar_Compiler_Util.starts_with - uu___20 ns) namespaces in + (FStar_Syntax_Syntax.fv_eq_lid + fv) lids in FStar_Compiler_Effect.op_Less_Bar - yesno uu___19 in - [uu___18] in - uu___16 :: uu___17 in - uu___14 :: uu___15 in - uu___12 :: uu___13 in - uu___10 :: uu___11 in - uu___8 :: uu___9 in - comb_or uu___7 in - meets_some_criterion)) - | uu___ -> default_unfolding ()) in - FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___1 -> - let uu___2 = FStar_Syntax_Print.fv_to_string fv in - let uu___3 = - let uu___4 = FStar_Syntax_Syntax.range_of_fv fv in - FStar_Compiler_Range_Ops.string_of_range uu___4 in - let uu___4 = string_of_res res in - FStar_Compiler_Util.print3 - "should_unfold: For %s (%s), unfolding res = %s\n" uu___2 - uu___3 uu___4); - (let r = - match res with - | (false, uu___1, uu___2) -> Should_unfold_no - | (true, false, false) -> Should_unfold_yes - | (true, true, false) -> Should_unfold_fully - | (true, false, true) -> Should_unfold_reify - | uu___1 -> - let uu___2 = - let uu___3 = string_of_res res in - FStar_Compiler_Util.format1 - "Unexpected unfolding result: %s" uu___3 in - FStar_Compiler_Effect.op_Less_Bar failwith uu___2 in - (let uu___2 = - ((((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_tac + fullyno uu___15 in + let uu___15 = + let uu___16 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + with + | FStar_Pervasives_Native.None -> no + | FStar_Pervasives_Native.Some qs -> + let uu___17 = + FStar_Compiler_Util.for_some + (fun q -> + FStar_Compiler_Util.for_some + (fun qual -> + let uu___18 = + FStar_Syntax_Print.qual_to_string + qual in + uu___18 = q) quals) + qs in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___17 in + let uu___17 = + let uu___18 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + with + | FStar_Pervasives_Native.None -> + no + | FStar_Pervasives_Native.Some + namespaces -> + let uu___19 = + FStar_Compiler_Util.for_some + (fun ns -> + let uu___20 = + let uu___21 = + FStar_Syntax_Syntax.lid_of_fv + fv in + FStar_Ident.nsstr + uu___21 in + FStar_Compiler_Util.starts_with + uu___20 ns) + namespaces in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___19 in + [uu___18] in + uu___16 :: uu___17 in + uu___14 :: uu___15 in + uu___12 :: uu___13 in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + comb_or uu___7 in + meets_some_criterion)) + | uu___ -> default_unfolding ()) in + FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___1 -> + let uu___2 = FStar_Syntax_Print.fv_to_string fv in + let uu___3 = + let uu___4 = FStar_Syntax_Syntax.range_of_fv fv in + FStar_Compiler_Range_Ops.string_of_range uu___4 in + let uu___4 = string_of_res res in + FStar_Compiler_Util.print3 + "should_unfold: For %s (%s), unfolding res = %s\n" uu___2 + uu___3 uu___4); + (let r = + match res with + | (false, uu___1, uu___2) -> Should_unfold_no + | (true, false, false) -> Should_unfold_yes + | (true, true, false) -> Should_unfold_fully + | (true, false, true) -> Should_unfold_reify + | uu___1 -> + let uu___2 = + let uu___3 = string_of_res res in + FStar_Compiler_Util.format1 + "Unexpected unfolding result: %s" uu___3 in + FStar_Compiler_Effect.op_Less_Bar failwith uu___2 in + (let uu___2 = + ((((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_tac + && + (let uu___3 = FStar_Options.no_plugins () in + Prims.op_Negation uu___3)) + && (r <> Should_unfold_no)) && - (let uu___3 = FStar_Options.no_plugins () in - Prims.op_Negation uu___3)) - && (r <> Should_unfold_no)) - && - (FStar_Compiler_Util.for_some - (FStar_Syntax_Util.is_fvar FStar_Parser_Const.plugin_attr) - attrs)) - && - (let uu___3 = - FStar_Compiler_Effect.op_Bang plugin_unfold_warn_ctr in - uu___3 > Prims.int_zero) in - if uu___2 - then - let msg = - let uu___3 = FStar_Syntax_Print.fv_to_string fv in - FStar_Compiler_Util.format1 - "Unfolding name which is marked as a plugin: %s" uu___3 in - (FStar_Errors.log_issue - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.p - (FStar_Errors_Codes.Warning_UnfoldPlugin, msg); - (let uu___4 = - let uu___5 = - FStar_Compiler_Effect.op_Bang plugin_unfold_warn_ctr in - uu___5 - Prims.int_one in - FStar_Compiler_Effect.op_Colon_Equals plugin_unfold_warn_ctr - uu___4)) - else ()); - r) + (FStar_Compiler_Util.for_some + (FStar_Syntax_Util.is_fvar + FStar_Parser_Const.plugin_attr) attrs)) + && + (let uu___3 = + FStar_Compiler_Effect.op_Bang plugin_unfold_warn_ctr in + uu___3 > Prims.int_zero) in + if uu___2 + then + let msg = + let uu___3 = FStar_Syntax_Print.fv_to_string fv in + FStar_Compiler_Util.format1 + "Unfolding name which is marked as a plugin: %s" uu___3 in + (FStar_Errors.log_issue + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.p + (FStar_Errors_Codes.Warning_UnfoldPlugin, msg); + (let uu___4 = + let uu___5 = + FStar_Compiler_Effect.op_Bang plugin_unfold_warn_ctr in + uu___5 - Prims.int_one in + FStar_Compiler_Effect.op_Colon_Equals + plugin_unfold_warn_ctr uu___4)) + else ()); + r) let decide_unfolding : 'uuuuu . FStar_TypeChecker_Cfg.cfg -> - stack_elt Prims.list -> - 'uuuuu -> - FStar_Syntax_Syntax.fv -> - FStar_TypeChecker_Env.qninfo -> - (FStar_TypeChecker_Cfg.cfg * stack_elt Prims.list) - FStar_Pervasives_Native.option + Prims.bool -> + stack_elt Prims.list -> + 'uuuuu -> + FStar_Syntax_Syntax.fv -> + FStar_TypeChecker_Env.qninfo -> + (FStar_TypeChecker_Cfg.cfg * stack_elt Prims.list) + FStar_Pervasives_Native.option = fun cfg -> - fun stack1 -> - fun rng -> - fun fv -> - fun qninfo -> - let res = - should_unfold cfg (fun cfg1 -> should_reify cfg1 stack1) fv - qninfo in - match res with - | Should_unfold_no -> FStar_Pervasives_Native.None - | Should_unfold_yes -> FStar_Pervasives_Native.Some (cfg, stack1) - | Should_unfold_fully -> - let cfg' = - { - FStar_TypeChecker_Cfg.steps = - (let uu___ = cfg.FStar_TypeChecker_Cfg.steps in - { - FStar_TypeChecker_Cfg.beta = - (uu___.FStar_TypeChecker_Cfg.beta); - FStar_TypeChecker_Cfg.iota = - (uu___.FStar_TypeChecker_Cfg.iota); - FStar_TypeChecker_Cfg.zeta = - (uu___.FStar_TypeChecker_Cfg.zeta); - FStar_TypeChecker_Cfg.zeta_full = - (uu___.FStar_TypeChecker_Cfg.zeta_full); - FStar_TypeChecker_Cfg.weak = - (uu___.FStar_TypeChecker_Cfg.weak); - FStar_TypeChecker_Cfg.hnf = - (uu___.FStar_TypeChecker_Cfg.hnf); - FStar_TypeChecker_Cfg.primops = - (uu___.FStar_TypeChecker_Cfg.primops); - FStar_TypeChecker_Cfg.do_not_unfold_pure_lets = - (uu___.FStar_TypeChecker_Cfg.do_not_unfold_pure_lets); - FStar_TypeChecker_Cfg.unfold_until = - (FStar_Pervasives_Native.Some - FStar_Syntax_Syntax.delta_constant); - FStar_TypeChecker_Cfg.unfold_only = - FStar_Pervasives_Native.None; - FStar_TypeChecker_Cfg.unfold_fully = - FStar_Pervasives_Native.None; - FStar_TypeChecker_Cfg.unfold_attr = - FStar_Pervasives_Native.None; - FStar_TypeChecker_Cfg.unfold_qual = - FStar_Pervasives_Native.None; - FStar_TypeChecker_Cfg.unfold_namespace = - FStar_Pervasives_Native.None; - FStar_TypeChecker_Cfg.unfold_tac = - (uu___.FStar_TypeChecker_Cfg.unfold_tac); - FStar_TypeChecker_Cfg.pure_subterms_within_computations - = - (uu___.FStar_TypeChecker_Cfg.pure_subterms_within_computations); - FStar_TypeChecker_Cfg.simplify = - (uu___.FStar_TypeChecker_Cfg.simplify); - FStar_TypeChecker_Cfg.erase_universes = - (uu___.FStar_TypeChecker_Cfg.erase_universes); - FStar_TypeChecker_Cfg.allow_unbound_universes = - (uu___.FStar_TypeChecker_Cfg.allow_unbound_universes); - FStar_TypeChecker_Cfg.reify_ = - (uu___.FStar_TypeChecker_Cfg.reify_); - FStar_TypeChecker_Cfg.compress_uvars = - (uu___.FStar_TypeChecker_Cfg.compress_uvars); - FStar_TypeChecker_Cfg.no_full_norm = - (uu___.FStar_TypeChecker_Cfg.no_full_norm); - FStar_TypeChecker_Cfg.check_no_uvars = - (uu___.FStar_TypeChecker_Cfg.check_no_uvars); - FStar_TypeChecker_Cfg.unmeta = - (uu___.FStar_TypeChecker_Cfg.unmeta); - FStar_TypeChecker_Cfg.unascribe = - (uu___.FStar_TypeChecker_Cfg.unascribe); - FStar_TypeChecker_Cfg.in_full_norm_request = - (uu___.FStar_TypeChecker_Cfg.in_full_norm_request); - FStar_TypeChecker_Cfg.weakly_reduce_scrutinee = - (uu___.FStar_TypeChecker_Cfg.weakly_reduce_scrutinee); - FStar_TypeChecker_Cfg.nbe_step = - (uu___.FStar_TypeChecker_Cfg.nbe_step); - FStar_TypeChecker_Cfg.for_extraction = - (uu___.FStar_TypeChecker_Cfg.for_extraction); - FStar_TypeChecker_Cfg.unrefine = - (uu___.FStar_TypeChecker_Cfg.unrefine) - }); - FStar_TypeChecker_Cfg.tcenv = - (cfg.FStar_TypeChecker_Cfg.tcenv); - FStar_TypeChecker_Cfg.debug = - (cfg.FStar_TypeChecker_Cfg.debug); - FStar_TypeChecker_Cfg.delta_level = - (cfg.FStar_TypeChecker_Cfg.delta_level); - FStar_TypeChecker_Cfg.primitive_steps = - (cfg.FStar_TypeChecker_Cfg.primitive_steps); - FStar_TypeChecker_Cfg.strong = - (cfg.FStar_TypeChecker_Cfg.strong); - FStar_TypeChecker_Cfg.memoize_lazy = - (cfg.FStar_TypeChecker_Cfg.memoize_lazy); - FStar_TypeChecker_Cfg.normalize_pure_lets = - (cfg.FStar_TypeChecker_Cfg.normalize_pure_lets); - FStar_TypeChecker_Cfg.reifying = - (cfg.FStar_TypeChecker_Cfg.reifying); - FStar_TypeChecker_Cfg.compat_memo_ignore_cfg = - (cfg.FStar_TypeChecker_Cfg.compat_memo_ignore_cfg) - } in - let stack' = - match stack1 with - | (UnivArgs (us, r))::stack'1 -> (UnivArgs (us, r)) :: - (Cfg (cfg, FStar_Pervasives_Native.None)) :: stack'1 - | stack'1 -> (Cfg (cfg, FStar_Pervasives_Native.None)) :: - stack'1 in - FStar_Pervasives_Native.Some (cfg', stack') - | Should_unfold_reify -> - let rec push e s = - match s with - | [] -> [e] - | (UnivArgs (us, r))::t -> - let uu___ = push e t in (UnivArgs (us, r)) :: uu___ - | h::t -> e :: h :: t in - let ref = - let uu___ = - let uu___1 = - let uu___2 = FStar_Syntax_Syntax.lid_of_fv fv in - FStar_Const.Const_reflect uu___2 in - FStar_Syntax_Syntax.Tm_constant uu___1 in - FStar_Syntax_Syntax.mk uu___ - FStar_Compiler_Range_Type.dummyRange in - let stack2 = - push - (App - (empty_env, ref, FStar_Pervasives_Native.None, - FStar_Compiler_Range_Type.dummyRange)) stack1 in - FStar_Pervasives_Native.Some (cfg, stack2) + fun strict_ok -> + fun stack1 -> + fun rng -> + fun fv -> + fun qninfo -> + let res = + should_unfold cfg strict_ok + (fun cfg1 -> should_reify cfg1 stack1) fv qninfo in + match res with + | Should_unfold_no -> FStar_Pervasives_Native.None + | Should_unfold_yes -> + FStar_Pervasives_Native.Some (cfg, stack1) + | Should_unfold_fully -> + let cfg' = + { + FStar_TypeChecker_Cfg.steps = + (let uu___ = cfg.FStar_TypeChecker_Cfg.steps in + { + FStar_TypeChecker_Cfg.beta = + (uu___.FStar_TypeChecker_Cfg.beta); + FStar_TypeChecker_Cfg.iota = + (uu___.FStar_TypeChecker_Cfg.iota); + FStar_TypeChecker_Cfg.zeta = + (uu___.FStar_TypeChecker_Cfg.zeta); + FStar_TypeChecker_Cfg.zeta_full = + (uu___.FStar_TypeChecker_Cfg.zeta_full); + FStar_TypeChecker_Cfg.weak = + (uu___.FStar_TypeChecker_Cfg.weak); + FStar_TypeChecker_Cfg.hnf = + (uu___.FStar_TypeChecker_Cfg.hnf); + FStar_TypeChecker_Cfg.primops = + (uu___.FStar_TypeChecker_Cfg.primops); + FStar_TypeChecker_Cfg.do_not_unfold_pure_lets = + (uu___.FStar_TypeChecker_Cfg.do_not_unfold_pure_lets); + FStar_TypeChecker_Cfg.unfold_until = + (FStar_Pervasives_Native.Some + FStar_Syntax_Syntax.delta_constant); + FStar_TypeChecker_Cfg.unfold_only = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_fully = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_attr = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_qual = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_namespace = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_tac = + (uu___.FStar_TypeChecker_Cfg.unfold_tac); + FStar_TypeChecker_Cfg.pure_subterms_within_computations + = + (uu___.FStar_TypeChecker_Cfg.pure_subterms_within_computations); + FStar_TypeChecker_Cfg.simplify = + (uu___.FStar_TypeChecker_Cfg.simplify); + FStar_TypeChecker_Cfg.erase_universes = + (uu___.FStar_TypeChecker_Cfg.erase_universes); + FStar_TypeChecker_Cfg.allow_unbound_universes = + (uu___.FStar_TypeChecker_Cfg.allow_unbound_universes); + FStar_TypeChecker_Cfg.reify_ = + (uu___.FStar_TypeChecker_Cfg.reify_); + FStar_TypeChecker_Cfg.compress_uvars = + (uu___.FStar_TypeChecker_Cfg.compress_uvars); + FStar_TypeChecker_Cfg.no_full_norm = + (uu___.FStar_TypeChecker_Cfg.no_full_norm); + FStar_TypeChecker_Cfg.check_no_uvars = + (uu___.FStar_TypeChecker_Cfg.check_no_uvars); + FStar_TypeChecker_Cfg.unmeta = + (uu___.FStar_TypeChecker_Cfg.unmeta); + FStar_TypeChecker_Cfg.unascribe = + (uu___.FStar_TypeChecker_Cfg.unascribe); + FStar_TypeChecker_Cfg.in_full_norm_request = + (uu___.FStar_TypeChecker_Cfg.in_full_norm_request); + FStar_TypeChecker_Cfg.weakly_reduce_scrutinee = + (uu___.FStar_TypeChecker_Cfg.weakly_reduce_scrutinee); + FStar_TypeChecker_Cfg.nbe_step = + (uu___.FStar_TypeChecker_Cfg.nbe_step); + FStar_TypeChecker_Cfg.for_extraction = + (uu___.FStar_TypeChecker_Cfg.for_extraction); + FStar_TypeChecker_Cfg.unrefine = + (uu___.FStar_TypeChecker_Cfg.unrefine) + }); + FStar_TypeChecker_Cfg.tcenv = + (cfg.FStar_TypeChecker_Cfg.tcenv); + FStar_TypeChecker_Cfg.debug = + (cfg.FStar_TypeChecker_Cfg.debug); + FStar_TypeChecker_Cfg.delta_level = + (cfg.FStar_TypeChecker_Cfg.delta_level); + FStar_TypeChecker_Cfg.primitive_steps = + (cfg.FStar_TypeChecker_Cfg.primitive_steps); + FStar_TypeChecker_Cfg.strong = + (cfg.FStar_TypeChecker_Cfg.strong); + FStar_TypeChecker_Cfg.memoize_lazy = + (cfg.FStar_TypeChecker_Cfg.memoize_lazy); + FStar_TypeChecker_Cfg.normalize_pure_lets = + (cfg.FStar_TypeChecker_Cfg.normalize_pure_lets); + FStar_TypeChecker_Cfg.reifying = + (cfg.FStar_TypeChecker_Cfg.reifying); + FStar_TypeChecker_Cfg.compat_memo_ignore_cfg = + (cfg.FStar_TypeChecker_Cfg.compat_memo_ignore_cfg) + } in + let stack' = + match stack1 with + | (UnivArgs (us, r))::stack'1 -> (UnivArgs (us, r)) :: + (Cfg (cfg, FStar_Pervasives_Native.None)) :: stack'1 + | stack'1 -> (Cfg (cfg, FStar_Pervasives_Native.None)) :: + stack'1 in + FStar_Pervasives_Native.Some (cfg', stack') + | Should_unfold_reify -> + let rec push e s = + match s with + | [] -> [e] + | (UnivArgs (us, r))::t -> + let uu___ = push e t in (UnivArgs (us, r)) :: uu___ + | h::t -> e :: h :: t in + let ref = + let uu___ = + let uu___1 = + let uu___2 = FStar_Syntax_Syntax.lid_of_fv fv in + FStar_Const.Const_reflect uu___2 in + FStar_Syntax_Syntax.Tm_constant uu___1 in + FStar_Syntax_Syntax.mk uu___ + FStar_Compiler_Range_Type.dummyRange in + let stack2 = + push + (App + (empty_env, ref, FStar_Pervasives_Native.None, + FStar_Compiler_Range_Type.dummyRange)) stack1 in + FStar_Pervasives_Native.Some (cfg, stack2) let (on_domain_lids : FStar_Ident.lident Prims.list) = [FStar_Parser_Const.fext_on_domain_lid; FStar_Parser_Const.fext_on_dom_lid; @@ -3071,8 +3140,8 @@ let rec (norm : rebuild cfg empty_env stack2 t1) | uu___3 -> let uu___4 = - decide_unfolding cfg stack2 t1.FStar_Syntax_Syntax.pos - fv qninfo in + decide_unfolding cfg false stack2 + t1.FStar_Syntax_Syntax.pos fv qninfo in (match uu___4 with | FStar_Pervasives_Native.Some (cfg1, stack3) -> do_unfold_fv cfg1 stack3 t1 qninfo fv @@ -3612,166 +3681,95 @@ let rec (norm : { FStar_Syntax_Syntax.hd = head; FStar_Syntax_Syntax.args = args;_} -> - let strict_args = - let uu___2 = - let uu___3 = - let uu___4 = - FStar_Compiler_Effect.op_Bar_Greater head - FStar_Syntax_Util.unascribe in - FStar_Compiler_Effect.op_Bar_Greater uu___4 - FStar_Syntax_Util.un_uinst in - uu___3.FStar_Syntax_Syntax.n in - match uu___2 with + let fallback uu___2 = + let stack3 = + FStar_Compiler_List.fold_right + (fun uu___3 -> + fun stack4 -> + match uu___3 with + | (a, aq) -> + let a1 = + let uu___4 = + (((let uu___5 = + FStar_TypeChecker_Cfg.cfg_env cfg in + uu___5.FStar_TypeChecker_Env.erase_erasable_args) + || + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction) + || + (cfg.FStar_TypeChecker_Cfg.debug).FStar_TypeChecker_Cfg.erase_erasable_args) + && + (FStar_Syntax_Util.aqual_is_erasable aq) in + if uu___4 + then FStar_Syntax_Util.exp_unit + else a in + let env2 = + let uu___4 = + let uu___5 = FStar_Syntax_Subst.compress a1 in + uu___5.FStar_Syntax_Syntax.n in + match uu___4 with + | FStar_Syntax_Syntax.Tm_name uu___5 -> + empty_env + | FStar_Syntax_Syntax.Tm_constant uu___5 -> + empty_env + | FStar_Syntax_Syntax.Tm_lazy uu___5 -> + empty_env + | FStar_Syntax_Syntax.Tm_fvar uu___5 -> + empty_env + | uu___5 -> env1 in + let uu___4 = + let uu___5 = + let uu___6 = + let uu___7 = + let uu___8 = + FStar_Compiler_Util.mk_ref + FStar_Pervasives_Native.None in + (env2, a1, uu___8, false) in + Clos uu___7 in + (uu___6, aq, (t1.FStar_Syntax_Syntax.pos)) in + Arg uu___5 in + uu___4 :: stack4) args stack2 in + FStar_TypeChecker_Cfg.log cfg + (fun uu___4 -> + let uu___5 = + FStar_Compiler_Effect.op_Less_Bar + FStar_Compiler_Util.string_of_int + (FStar_Compiler_List.length args) in + FStar_Compiler_Util.print1 "\tPushed %s arguments\n" + uu___5); + norm cfg env1 stack3 head in + let head_fv_us_opt = + let head1 = FStar_Syntax_Util.unascribe head in + let head2 = FStar_Syntax_Subst.compress head1 in + match head2.FStar_Syntax_Syntax.n with | FStar_Syntax_Syntax.Tm_fvar fv -> - FStar_TypeChecker_Env.fv_has_strict_args - cfg.FStar_TypeChecker_Cfg.tcenv fv - | uu___3 -> FStar_Pervasives_Native.None in - (match strict_args with - | FStar_Pervasives_Native.None -> - let stack3 = - FStar_Compiler_List.fold_right - (fun uu___2 -> - fun stack4 -> - match uu___2 with - | (a, aq) -> - let a1 = - let uu___3 = - (((let uu___4 = - FStar_TypeChecker_Cfg.cfg_env cfg in - uu___4.FStar_TypeChecker_Env.erase_erasable_args) - || - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction) - || - (cfg.FStar_TypeChecker_Cfg.debug).FStar_TypeChecker_Cfg.erase_erasable_args) - && - (FStar_Syntax_Util.aqual_is_erasable - aq) in - if uu___3 - then FStar_Syntax_Util.exp_unit - else a in - let env2 = - let uu___3 = - let uu___4 = - FStar_Syntax_Subst.compress a1 in - uu___4.FStar_Syntax_Syntax.n in - match uu___3 with - | FStar_Syntax_Syntax.Tm_name uu___4 -> - empty_env - | FStar_Syntax_Syntax.Tm_constant uu___4 - -> empty_env - | FStar_Syntax_Syntax.Tm_lazy uu___4 -> - empty_env - | FStar_Syntax_Syntax.Tm_fvar uu___4 -> - empty_env - | uu___4 -> env1 in - let uu___3 = - let uu___4 = - let uu___5 = - let uu___6 = - let uu___7 = - FStar_Compiler_Util.mk_ref - FStar_Pervasives_Native.None in - (env2, a1, uu___7, false) in - Clos uu___6 in - (uu___5, aq, - (t1.FStar_Syntax_Syntax.pos)) in - Arg uu___4 in - uu___3 :: stack4) args stack2 in - (FStar_TypeChecker_Cfg.log cfg - (fun uu___3 -> - let uu___4 = - FStar_Compiler_Effect.op_Less_Bar - FStar_Compiler_Util.string_of_int - (FStar_Compiler_List.length args) in - FStar_Compiler_Util.print1 - "\tPushed %s arguments\n" uu___4); - norm cfg env1 stack3 head) - | FStar_Pervasives_Native.Some strict_args1 -> - let norm_args = - FStar_Compiler_Effect.op_Bar_Greater args - (FStar_Compiler_List.map - (fun uu___2 -> - match uu___2 with - | (a, i) -> - let uu___3 = norm cfg env1 [] a in - (uu___3, i))) in - let norm_args_len = FStar_Compiler_List.length norm_args in + FStar_Pervasives_Native.Some (head2, fv, []) + | FStar_Syntax_Syntax.Tm_uinst + ({ + FStar_Syntax_Syntax.n = FStar_Syntax_Syntax.Tm_fvar + fv; + FStar_Syntax_Syntax.pos = uu___2; + FStar_Syntax_Syntax.vars = uu___3; + FStar_Syntax_Syntax.hash_code = uu___4;_}, + us) + -> + FStar_Pervasives_Native.Some + ((FStar_Pervasives_Native.fst + (FStar_Syntax_Syntax.__proj__Tm_uinst__item___0 + head2.FStar_Syntax_Syntax.n)), fv, us) + | uu___2 -> FStar_Pervasives_Native.None in + (match head_fv_us_opt with + | FStar_Pervasives_Native.None -> fallback () + | FStar_Pervasives_Native.Some (head1, fv, us) -> let uu___2 = - FStar_Compiler_Effect.op_Bar_Greater strict_args1 - (FStar_Compiler_List.for_all - (fun i -> - if i >= norm_args_len - then false - else - (let uu___4 = - FStar_Compiler_List.nth norm_args i in - match uu___4 with - | (arg_i, uu___5) -> - let uu___6 = - let uu___7 = - FStar_Compiler_Effect.op_Bar_Greater - arg_i - FStar_Syntax_Util.unmeta_safe in - FStar_Compiler_Effect.op_Bar_Greater - uu___7 - FStar_Syntax_Util.head_and_args in - (match uu___6 with - | (head1, uu___7) -> - let uu___8 = - let uu___9 = - FStar_Syntax_Util.un_uinst - head1 in - uu___9.FStar_Syntax_Syntax.n in - (match uu___8 with - | FStar_Syntax_Syntax.Tm_constant - uu___9 -> true - | FStar_Syntax_Syntax.Tm_fvar fv - -> - let uu___9 = - FStar_Syntax_Syntax.lid_of_fv - fv in - FStar_TypeChecker_Env.is_datacon - cfg.FStar_TypeChecker_Cfg.tcenv - uu___9 - | uu___9 -> false))))) in - if uu___2 - then - let stack3 = - FStar_Compiler_Effect.op_Bar_Greater stack2 - (FStar_Compiler_List.fold_right - (fun uu___3 -> - fun stack4 -> - match uu___3 with - | (a, aq) -> - let uu___4 = - let uu___5 = - let uu___6 = - let uu___7 = - let uu___8 = - FStar_Compiler_Util.mk_ref - (FStar_Pervasives_Native.Some - (cfg, ([], a))) in - (env1, a, uu___8, false) in - Clos uu___7 in - (uu___6, aq, - (t1.FStar_Syntax_Syntax.pos)) in - Arg uu___5 in - uu___4 :: stack4) norm_args) in - (FStar_TypeChecker_Cfg.log cfg - (fun uu___4 -> - let uu___5 = - FStar_Compiler_Effect.op_Less_Bar - FStar_Compiler_Util.string_of_int - (FStar_Compiler_List.length args) in - FStar_Compiler_Util.print1 - "\tPushed %s arguments\n" uu___5); - norm cfg env1 stack3 head) - else - (let head1 = closure_as_term cfg env1 head in - let term = - FStar_Syntax_Syntax.mk_Tm_app head1 norm_args - t1.FStar_Syntax_Syntax.pos in - rebuild cfg env1 stack2 term)) + FStar_TypeChecker_Env.fv_has_strict_args + cfg.FStar_TypeChecker_Cfg.tcenv fv in + (match uu___2 with + | FStar_Pervasives_Native.Some + (strict_unfold, strict_args) -> + handle_strict_application cfg env1 stack2 head1 fv + us strict_unfold strict_args args + t1.FStar_Syntax_Syntax.pos + | FStar_Pervasives_Native.None -> fallback ())) | FStar_Syntax_Syntax.Tm_refine { FStar_Syntax_Syntax.b = x; FStar_Syntax_Syntax.phi = uu___2;_} @@ -4712,19 +4710,22 @@ and (do_unfold_fv : then match stack1 with | (UnivArgs (us', uu___2))::stack2 -> - ((let uu___4 = + (if n <> (FStar_Compiler_List.length us') + then failwith "ah!!!" + else (); + (let uu___5 = FStar_Compiler_Effect.op_Less_Bar (FStar_TypeChecker_Env.debug cfg.FStar_TypeChecker_Cfg.tcenv) (FStar_Options.Other "univ_norm") in - if uu___4 + if uu___5 then FStar_Compiler_List.iter (fun x -> - let uu___5 = + let uu___6 = FStar_Syntax_Print.univ_to_string x in FStar_Compiler_Util.print1 - "Univ (normalizer) %s\n" uu___5) us' + "Univ (normalizer) %s\n" uu___6) us' else ()); (let env1 = FStar_Compiler_Effect.op_Bar_Greater us' @@ -4741,15 +4742,312 @@ and (do_unfold_fv : (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.allow_unbound_universes -> norm cfg empty_env stack1 t1 | uu___2 -> - let uu___3 = - let uu___4 = - FStar_Syntax_Print.lid_to_string - (f.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in - FStar_Compiler_Util.format1 - "Impossible: missing universe instantiation on %s" - uu___4 in - failwith uu___3 - else norm cfg empty_env stack1 t1)) + (FStar_TypeChecker_Cfg.log cfg + (fun uu___4 -> + let uu___5 = + let uu___6 = + let uu___7 = + firstn (Prims.of_int (4)) stack1 in + FStar_Compiler_Effect.op_Less_Bar + FStar_Pervasives_Native.fst uu___7 in + stack_to_string uu___6 in + FStar_Compiler_Util.print1 + "top of stack = %s\n" uu___5); + (let uu___4 = + let uu___5 = + FStar_Syntax_Print.lid_to_string + (f.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in + FStar_Compiler_Util.format1 + "Impossible: missing universe instantiation on %s" + uu___5 in + failwith uu___4)) + else + (match stack1 with + | (UnivArgs (us', uu___3))::stack2 -> + failwith "univ args on not-uni-poly defn?" + | uu___3 -> norm cfg empty_env stack1 t1))) +and (handle_strict_application : + FStar_TypeChecker_Cfg.cfg -> + env -> + stack_elt Prims.list -> + FStar_Syntax_Syntax.term -> + FStar_Syntax_Syntax.fv -> + FStar_Syntax_Syntax.universes -> + Prims.bool -> + Prims.int Prims.list -> + (FStar_Syntax_Syntax.term' FStar_Syntax_Syntax.syntax * + FStar_Syntax_Syntax.arg_qualifier + FStar_Pervasives_Native.option) Prims.list -> + FStar_Compiler_Range_Type.range -> + FStar_Syntax_Syntax.term) + = + fun cfg -> + fun env1 -> + fun stack1 -> + fun head -> + fun fv -> + fun us -> + fun strict_unfold -> + fun strict_args -> + fun args -> + fun rng -> + FStar_TypeChecker_Cfg.log cfg + (fun uu___1 -> + let uu___2 = FStar_Syntax_Print.fv_to_string fv in + let uu___3 = + (FStar_Common.string_of_list ()) + FStar_Compiler_Util.string_of_int strict_args in + let uu___4 = + FStar_Compiler_Util.string_of_bool strict_unfold in + FStar_Compiler_Util.print3 + "Got strict application for %s, strict_args = %s, strict_unfold = %s\n" + uu___2 uu___3 uu___4); + (let cfg_args = + if strict_unfold + then + { + FStar_TypeChecker_Cfg.steps = + (let uu___1 = cfg.FStar_TypeChecker_Cfg.steps in + { + FStar_TypeChecker_Cfg.beta = + (uu___1.FStar_TypeChecker_Cfg.beta); + FStar_TypeChecker_Cfg.iota = + (uu___1.FStar_TypeChecker_Cfg.iota); + FStar_TypeChecker_Cfg.zeta = + (uu___1.FStar_TypeChecker_Cfg.zeta); + FStar_TypeChecker_Cfg.zeta_full = + (uu___1.FStar_TypeChecker_Cfg.zeta_full); + FStar_TypeChecker_Cfg.weak = true; + FStar_TypeChecker_Cfg.hnf = true; + FStar_TypeChecker_Cfg.primops = + (uu___1.FStar_TypeChecker_Cfg.primops); + FStar_TypeChecker_Cfg.do_not_unfold_pure_lets + = + (uu___1.FStar_TypeChecker_Cfg.do_not_unfold_pure_lets); + FStar_TypeChecker_Cfg.unfold_until = + (FStar_Pervasives_Native.Some + FStar_Syntax_Syntax.delta_constant); + FStar_TypeChecker_Cfg.unfold_only = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_fully = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_attr = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_qual = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_namespace = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_tac = + (uu___1.FStar_TypeChecker_Cfg.unfold_tac); + FStar_TypeChecker_Cfg.pure_subterms_within_computations + = + (uu___1.FStar_TypeChecker_Cfg.pure_subterms_within_computations); + FStar_TypeChecker_Cfg.simplify = + (uu___1.FStar_TypeChecker_Cfg.simplify); + FStar_TypeChecker_Cfg.erase_universes = + (uu___1.FStar_TypeChecker_Cfg.erase_universes); + FStar_TypeChecker_Cfg.allow_unbound_universes + = + (uu___1.FStar_TypeChecker_Cfg.allow_unbound_universes); + FStar_TypeChecker_Cfg.reify_ = + (uu___1.FStar_TypeChecker_Cfg.reify_); + FStar_TypeChecker_Cfg.compress_uvars = + (uu___1.FStar_TypeChecker_Cfg.compress_uvars); + FStar_TypeChecker_Cfg.no_full_norm = + (uu___1.FStar_TypeChecker_Cfg.no_full_norm); + FStar_TypeChecker_Cfg.check_no_uvars = + (uu___1.FStar_TypeChecker_Cfg.check_no_uvars); + FStar_TypeChecker_Cfg.unmeta = + (uu___1.FStar_TypeChecker_Cfg.unmeta); + FStar_TypeChecker_Cfg.unascribe = + (uu___1.FStar_TypeChecker_Cfg.unascribe); + FStar_TypeChecker_Cfg.in_full_norm_request + = + (uu___1.FStar_TypeChecker_Cfg.in_full_norm_request); + FStar_TypeChecker_Cfg.weakly_reduce_scrutinee + = + (uu___1.FStar_TypeChecker_Cfg.weakly_reduce_scrutinee); + FStar_TypeChecker_Cfg.nbe_step = + (uu___1.FStar_TypeChecker_Cfg.nbe_step); + FStar_TypeChecker_Cfg.for_extraction = + (uu___1.FStar_TypeChecker_Cfg.for_extraction); + FStar_TypeChecker_Cfg.unrefine = + (uu___1.FStar_TypeChecker_Cfg.unrefine) + }); + FStar_TypeChecker_Cfg.tcenv = + (cfg.FStar_TypeChecker_Cfg.tcenv); + FStar_TypeChecker_Cfg.debug = + (cfg.FStar_TypeChecker_Cfg.debug); + FStar_TypeChecker_Cfg.delta_level = + [FStar_TypeChecker_Env.Unfold + FStar_Syntax_Syntax.delta_constant]; + FStar_TypeChecker_Cfg.primitive_steps = + (cfg.FStar_TypeChecker_Cfg.primitive_steps); + FStar_TypeChecker_Cfg.strong = + (cfg.FStar_TypeChecker_Cfg.strong); + FStar_TypeChecker_Cfg.memoize_lazy = + (cfg.FStar_TypeChecker_Cfg.memoize_lazy); + FStar_TypeChecker_Cfg.normalize_pure_lets = + (cfg.FStar_TypeChecker_Cfg.normalize_pure_lets); + FStar_TypeChecker_Cfg.reifying = + (cfg.FStar_TypeChecker_Cfg.reifying); + FStar_TypeChecker_Cfg.compat_memo_ignore_cfg = + (cfg.FStar_TypeChecker_Cfg.compat_memo_ignore_cfg) + } + else cfg in + let args_len = FStar_Compiler_List.length args in + let norm_args = + FStar_Compiler_Effect.op_Bar_Greater args + (FStar_Compiler_List.mapi + (fun idx -> + fun uu___1 -> + match uu___1 with + | (a, i) -> + let a1 = + FStar_TypeChecker_Cfg.log cfg + (fun uu___3 -> + let uu___4 = + FStar_Compiler_Util.string_of_int + idx in + let uu___5 = + FStar_Syntax_Print.term_to_string + a in + FStar_Compiler_Util.print2 + "Normalizing strict arg %s (%s)\n" + uu___4 uu___5); + if + strict_unfold && + (FStar_Compiler_List.mem idx + strict_args) + then norm cfg_args env1 [] a + else norm cfg env1 [] a in + (a1, i))) in + let is_hnf i = + if i >= args_len + then false + else + (let uu___2 = FStar_Compiler_List.nth norm_args i in + match uu___2 with + | (arg_i, uu___3) -> + let uu___4 = + let uu___5 = + FStar_Compiler_Effect.op_Bar_Greater + arg_i FStar_Syntax_Util.unmeta_safe in + FStar_Compiler_Effect.op_Bar_Greater uu___5 + FStar_Syntax_Util.head_and_args in + (match uu___4 with + | (head1, uu___5) -> + let uu___6 = + let uu___7 = + FStar_Syntax_Util.un_uinst head1 in + uu___7.FStar_Syntax_Syntax.n in + (match uu___6 with + | FStar_Syntax_Syntax.Tm_constant + uu___7 -> true + | FStar_Syntax_Syntax.Tm_fvar fv1 -> + let uu___7 = + FStar_Syntax_Syntax.lid_of_fv fv1 in + FStar_TypeChecker_Env.is_datacon + cfg.FStar_TypeChecker_Cfg.tcenv + uu___7 + | uu___7 -> false))) in + let uu___1 = + FStar_Compiler_List.for_all is_hnf strict_args in + if uu___1 + then + (FStar_TypeChecker_Cfg.log cfg + (fun uu___3 -> + let uu___4 = + FStar_Syntax_Print.term_to_string head in + let uu___5 = + FStar_Syntax_Print.univs_to_string us in + FStar_Compiler_Util.print2 + "Strict reduction kicking in for %s<%s>\n" + uu___4 uu___5); + (let lid = + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in + let qninfo = + FStar_TypeChecker_Env.lookup_qname + cfg.FStar_TypeChecker_Cfg.tcenv lid in + let stack2 = + FStar_Compiler_Effect.op_Bar_Greater stack1 + (FStar_Compiler_List.fold_right + (fun uu___3 -> + fun stack3 -> + match uu___3 with + | (a, aq) -> + let uu___4 = + let uu___5 = + let uu___6 = + let uu___7 = + let uu___8 = + FStar_Compiler_Util.mk_ref + (FStar_Pervasives_Native.Some + (cfg, ([], a))) in + (env1, a, uu___8, false) in + Clos uu___7 in + (uu___6, aq, rng) in + Arg uu___5 in + uu___4 :: stack3) norm_args) in + FStar_TypeChecker_Cfg.log cfg + (fun uu___4 -> + let uu___5 = + FStar_Compiler_Effect.op_Less_Bar + FStar_Compiler_Util.string_of_int + (FStar_Compiler_List.length args) in + FStar_Compiler_Util.print1 + "\tPushed %s arguments\n" uu___5); + (let stack3 = + match us with + | [] -> stack2 + | us1 -> + let us2 = + FStar_Compiler_List.map + (norm_universe cfg env1) us1 in + (UnivArgs + (us2, (head.FStar_Syntax_Syntax.pos))) + :: stack2 in + let head1 = FStar_Syntax_Subst.compress head in + let uu___4 = + decide_unfolding cfg true stack3 + head1.FStar_Syntax_Syntax.pos fv qninfo in + match uu___4 with + | FStar_Pervasives_Native.Some (cfg1, stack4) -> + do_unfold_fv cfg1 stack4 head1 qninfo fv + | FStar_Pervasives_Native.None -> + rebuild cfg env1 stack3 head1))) + else + (FStar_TypeChecker_Cfg.log cfg + (fun uu___4 -> + let uu___5 = + FStar_Syntax_Print.term_to_string head in + let uu___6 = + FStar_Syntax_Print.univs_to_string us in + FStar_Compiler_Util.print2 + "Strict reduction DID NOT kick in for %s<%s>, rebuilding\n" + uu___5 uu___6); + (let head1 = + match us with + | [] -> head + | us1 -> + FStar_Syntax_Syntax.mk_Tm_uinst head us1 in + let head2 = closure_as_term cfg env1 head1 in + let norm_args1 = + if false && strict_unfold + then + FStar_Compiler_Effect.op_Bar_Greater args + (FStar_Compiler_List.mapi + (fun idx -> + fun uu___4 -> + match uu___4 with + | (a, i) -> + let a1 = norm cfg env1 [] a in + (a1, i))) + else norm_args in + let term = + FStar_Syntax_Syntax.mk_Tm_app head2 norm_args1 + rng in + rebuild cfg env1 stack1 term))) and (reduce_impure_comp : FStar_TypeChecker_Cfg.cfg -> env -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml index 028e772a155..9dd049692fd 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml @@ -1562,7 +1562,68 @@ let (tc_sig_let : FStar_Syntax_Syntax.sigopts = (se1.FStar_Syntax_Syntax.sigopts) } in - let postprocess_lb tau lb = + let tcnorm env2 e2 = + let uu___4 = + let uu___5 = FStar_Options.tcnorm () in + Prims.op_Negation uu___5 in + if uu___4 + then + ((let uu___6 = + FStar_TypeChecker_Env.debug env2 + FStar_Options.Medium in + if uu___6 + then + let uu___7 = + let uu___8 = + FStar_Errors_Msg.text + "No tcnorm: it is disabled" in + [uu___8] in + FStar_Errors.diag_doc + se2.FStar_Syntax_Syntax.sigrng uu___7 + else ()); + e2) + else + (let e' = + FStar_TypeChecker_Normalize.normalize + [FStar_TypeChecker_Env.UnfoldAttr + [FStar_Parser_Const.tcnorm_attr]; + FStar_TypeChecker_Env.Exclude + FStar_TypeChecker_Env.Zeta; + FStar_TypeChecker_Env.UnfoldUntil + FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.NoFullNorm; + FStar_TypeChecker_Env.DoNotUnfoldPureLets] + env2 e2 in + (let uu___7 = + FStar_TypeChecker_Env.debug env2 + FStar_Options.Medium in + if uu___7 + then + let uu___8 = + let uu___9 = + let uu___10 = + FStar_Errors_Msg.text + "Before tcnorm =" in + let uu___11 = + FStar_Syntax_Print.term_to_doc e2 in + FStar_Pprint.op_Hat_Slash_Hat uu___10 + uu___11 in + let uu___10 = + let uu___11 = + let uu___12 = + FStar_Errors_Msg.text + "After tcnorm =" in + let uu___13 = + FStar_Syntax_Print.term_to_doc e' in + FStar_Pprint.op_Hat_Slash_Hat + uu___12 uu___13 in + [uu___11] in + uu___9 :: uu___10 in + FStar_Errors.diag_doc + se2.FStar_Syntax_Syntax.sigrng uu___8 + else ()); + e') in + let on_open_lbdef env2 f lb = let uu___4 = FStar_Syntax_Subst.univ_var_opening lb.FStar_Syntax_Syntax.lbunivs in @@ -1574,12 +1635,10 @@ let (tc_sig_let : let lbtyp = FStar_Syntax_Subst.subst s lb.FStar_Syntax_Syntax.lbtyp in - let env2 = - FStar_TypeChecker_Env.push_univ_vars env1 + let env3 = + FStar_TypeChecker_Env.push_univ_vars env2 univnames in - let lbdef1 = - FStar_TypeChecker_Env.postprocess env2 tau - lbtyp lbdef in + let lbdef1 = f env3 lbtyp lbdef in let lbdef2 = FStar_Syntax_Subst.close_univ_vars univnames lbdef1 in @@ -1784,16 +1843,33 @@ let (tc_sig_let : ((FStar_Pervasives_Native.fst lbs1), uu___10) in let lbs3 = + let uu___10 = + FStar_Compiler_Effect.op_Bar_Greater + (FStar_Pervasives_Native.snd lbs2) + (FStar_Compiler_List.map + (on_open_lbdef env1 + (fun env2 -> + fun _typ -> + fun tm -> tcnorm env2 tm))) in + ((FStar_Pervasives_Native.fst lbs2), + uu___10) in + let lbs4 = let uu___10 = match post_tau with | FStar_Pervasives_Native.Some tau -> - FStar_Compiler_List.map - (postprocess_lb tau) + FStar_Compiler_Effect.op_Bar_Greater (FStar_Pervasives_Native.snd - lbs2) + lbs3) + (FStar_Compiler_List.map + (on_open_lbdef env1 + (fun env2 -> + fun typ -> + fun tm -> + FStar_TypeChecker_Env.postprocess + env2 tau typ tm))) | FStar_Pervasives_Native.None -> - FStar_Pervasives_Native.snd lbs2 in - ((FStar_Pervasives_Native.fst lbs2), + FStar_Pervasives_Native.snd lbs3 in + ((FStar_Pervasives_Native.fst lbs3), uu___10) in let quals1 = match e2.FStar_Syntax_Syntax.n with @@ -1810,7 +1886,7 @@ let (tc_sig_let : FStar_Syntax_Syntax.sigel = (FStar_Syntax_Syntax.Sig_let { - FStar_Syntax_Syntax.lbs1 = lbs3; + FStar_Syntax_Syntax.lbs1 = lbs4; FStar_Syntax_Syntax.lids1 = lids }); FStar_Syntax_Syntax.sigrng = @@ -1825,7 +1901,7 @@ let (tc_sig_let : (se2.FStar_Syntax_Syntax.sigopens_and_abbrevs); FStar_Syntax_Syntax.sigopts = (se2.FStar_Syntax_Syntax.sigopts) - }, lbs3))) + }, lbs4))) | uu___5 -> failwith "impossible (typechecking should preserve Tm_let)" in @@ -4924,7 +5000,7 @@ let (tc_decls : ([], env) ses) in match uu___ with | (ses1, env1) -> ((FStar_Compiler_List.rev_append ses1 []), env1) -let (uu___905 : unit) = +let (uu___925 : unit) = FStar_Compiler_Effect.op_Colon_Equals tc_decls_knot (FStar_Pervasives_Native.Some tc_decls) let (snapshot_context : diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml index 0d762306efe..6041ee0d209 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml @@ -3624,7 +3624,7 @@ and (tc_match : env (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in FStar_Pervasives_Native.Some uu___10) () - with | uu___10 -> FStar_Pervasives_Native.None in + with | uu___9 -> FStar_Pervasives_Native.None in (match r with | FStar_Pervasives_Native.Some (us, t) -> let uu___9 = @@ -9830,83 +9830,88 @@ and (tc_eqn : (c2, FStar_TypeChecker_Env.trivial_guard) else - (match (eqs, - when_condition) - with - | uu___16 when - let uu___17 = - FStar_TypeChecker_Env.should_verify - pat_env in - Prims.op_Negation - uu___17 - -> - (c1, g_when) - | (FStar_Pervasives_Native.None, - FStar_Pervasives_Native.None) - -> - (c1, g_when) - | (FStar_Pervasives_Native.Some - f, - FStar_Pervasives_Native.None) - -> - let gf = - FStar_TypeChecker_Common.NonTrivial - f in - let g = - FStar_TypeChecker_Env.guard_of_guard_formula - gf in - let uu___16 = - FStar_TypeChecker_Util.weaken_precondition - pat_env c1 - gf in - let uu___17 = - FStar_TypeChecker_Env.imp_guard - g g_when in - (uu___16, - uu___17) - | (FStar_Pervasives_Native.Some - f, - FStar_Pervasives_Native.Some - w) -> - let g_f = - FStar_TypeChecker_Common.NonTrivial - f in - let g_fw = + if + (let uu___16 = + FStar_TypeChecker_Env.should_verify + pat_env in + Prims.op_Negation + uu___16) + then (c1, g_when) + else + (match (eqs, + when_condition) + with + | (FStar_Pervasives_Native.None, + FStar_Pervasives_Native.None) + -> + (c1, g_when) + | (FStar_Pervasives_Native.Some + f, + FStar_Pervasives_Native.None) + -> + let gf = + FStar_TypeChecker_Common.NonTrivial + f in + let g = + FStar_TypeChecker_Env.guard_of_guard_formula + gf in let uu___16 = - FStar_Syntax_Util.mk_conj + FStar_TypeChecker_Util.weaken_precondition + pat_env + c1 gf in + let uu___17 + = + FStar_TypeChecker_Env.imp_guard + g g_when in + (uu___16, + uu___17) + | (FStar_Pervasives_Native.Some + f, + FStar_Pervasives_Native.Some + w) -> + let g_f = + FStar_TypeChecker_Common.NonTrivial + f in + let g_fw = + let uu___16 + = + FStar_Syntax_Util.mk_conj f w in - FStar_TypeChecker_Common.NonTrivial - uu___16 in - let uu___16 = - FStar_TypeChecker_Util.weaken_precondition - pat_env c1 - g_fw in - let uu___17 = - let uu___18 + FStar_TypeChecker_Common.NonTrivial + uu___16 in + let uu___16 = - FStar_TypeChecker_Env.guard_of_guard_formula + FStar_TypeChecker_Util.weaken_precondition + pat_env + c1 g_fw in + let uu___17 + = + let uu___18 + = + FStar_TypeChecker_Env.guard_of_guard_formula g_f in - FStar_TypeChecker_Env.imp_guard - uu___18 - g_when in - (uu___16, - uu___17) - | (FStar_Pervasives_Native.None, - FStar_Pervasives_Native.Some - w) -> - let g_w = - FStar_TypeChecker_Common.NonTrivial - w in - let g = - FStar_TypeChecker_Env.guard_of_guard_formula - g_w in - let uu___16 = - FStar_TypeChecker_Util.weaken_precondition - pat_env c1 - g_w in - (uu___16, - g_when)) in + FStar_TypeChecker_Env.imp_guard + uu___18 + g_when in + (uu___16, + uu___17) + | (FStar_Pervasives_Native.None, + FStar_Pervasives_Native.Some + w) -> + let g_w = + FStar_TypeChecker_Common.NonTrivial + w in + let g = + FStar_TypeChecker_Env.guard_of_guard_formula + g_w in + let uu___16 + = + FStar_TypeChecker_Util.weaken_precondition + pat_env + c1 g_w in + (uu___16, + g_when)) in (match uu___14 with | (c_weak, g_when_weak) -> @@ -10468,10 +10473,8 @@ and (check_top_level_let : if uu___4 then FStar_TypeChecker_Normalize.normalize - [FStar_TypeChecker_Env.UnfoldAttr - [FStar_Parser_Const.tcnorm_attr]; - FStar_TypeChecker_Env.Exclude - FStar_TypeChecker_Env.Beta; + [FStar_TypeChecker_Env.Exclude + FStar_TypeChecker_Env.Beta; FStar_TypeChecker_Env.Exclude FStar_TypeChecker_Env.Zeta; FStar_TypeChecker_Env.NoFullNorm;