From bca036a67810e54835f0fb6bde0a31aa487122a6 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Thu, 3 Oct 2024 12:29:29 -0700 Subject: [PATCH] a bit of cleanup, adding some comments --- .../generated/FStar_Extraction_ML_Code.ml | 2 +- .../generated/FStar_Extraction_ML_Term.ml | 777 +++++++++--------- src/extraction/FStar.Extraction.ML.Code.fst | 2 +- src/extraction/FStar.Extraction.ML.Term.fst | 30 +- 4 files changed, 391 insertions(+), 420 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml index 7ef1639c852..f688a4c826a 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Code.ml @@ -495,7 +495,7 @@ let rec (doc_of_mltype' : let d1 = doc_of_mltype currentModule (t_prio_fun, Left) t1 in let d2 = doc_of_mltype currentModule (t_prio_fun, Right) t2 in let uu___ = - let uu___1 = reduce1 [d1; text "->"; d2] in hbox uu___1 in + let uu___1 = reduce1 [d1; text " -> "; d2] in hbox uu___1 in maybe_paren outer t_prio_fun uu___ | FStar_Extraction_ML_Syntax.MLTY_Top -> let uu___ = FStar_Extraction_ML_Util.codegen_fsharp () in diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml index 3f18501bf5c..d066ced9222 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Term.ml @@ -2289,325 +2289,316 @@ let rec (extract_lb_sig : uu___8) in (match uu___6 with | (tbinders, eff_body, tbody) -> - (FStar_Extraction_ML_UEnv.debug g - (fun uu___8 -> - let uu___9 = - FStar_Class_Show.show - FStar_Syntax_Print.showable_term tbody in - FStar_Compiler_Util.print1 - "Extract LB SIG: %s\n" uu___9); - (let n_tbinders = - FStar_Compiler_List.length tbinders in - let lbdef1 = - let uu___8 = normalize_abs lbdef in - FStar_Syntax_Util.unmeta uu___8 in - let tbinders_as_ty_params env = - FStar_Compiler_List.map - (fun uu___8 -> - match uu___8 with - | { FStar_Syntax_Syntax.binder_bv = x; - FStar_Syntax_Syntax.binder_qual = - uu___9; - FStar_Syntax_Syntax.binder_positivity - = uu___10; - FStar_Syntax_Syntax.binder_attrs = - binder_attrs;_} - -> + let n_tbinders = + FStar_Compiler_List.length tbinders in + let lbdef1 = + let uu___7 = normalize_abs lbdef in + FStar_Syntax_Util.unmeta uu___7 in + let tbinders_as_ty_params env = + FStar_Compiler_List.map + (fun uu___7 -> + match uu___7 with + | { FStar_Syntax_Syntax.binder_bv = x; + FStar_Syntax_Syntax.binder_qual = + uu___8; + FStar_Syntax_Syntax.binder_positivity + = uu___9; + FStar_Syntax_Syntax.binder_attrs = + binder_attrs;_} + -> + let uu___10 = let uu___11 = - let uu___12 = - FStar_Extraction_ML_UEnv.lookup_ty - env x in - uu___12.FStar_Extraction_ML_UEnv.ty_b_name in - let uu___12 = - FStar_Compiler_List.map - (fun attr -> - let uu___13 = - term_as_mlexpr g attr in - match uu___13 with - | (e, uu___14, uu___15) -> e) - binder_attrs in - { - FStar_Extraction_ML_Syntax.ty_param_name - = uu___11; - FStar_Extraction_ML_Syntax.ty_param_attrs - = uu___12 - }) in - match lbdef1.FStar_Syntax_Syntax.n with - | FStar_Syntax_Syntax.Tm_abs - { FStar_Syntax_Syntax.bs = bs2; - FStar_Syntax_Syntax.body = body; - FStar_Syntax_Syntax.rc_opt = copt;_} - -> - let uu___8 = - FStar_Syntax_Subst.open_term bs2 body in - (match uu___8 with - | (bs3, body1) -> - if - n_tbinders <= - (FStar_Compiler_List.length bs3) - then - let uu___9 = - FStar_Compiler_Util.first_N - n_tbinders bs3 in - (match uu___9 with - | (targs, rest_args) -> - let expected_source_ty = - let s = - FStar_Compiler_List.map2 - (fun uu___10 -> - fun uu___11 -> - match (uu___10, - uu___11) - with - | ({ - FStar_Syntax_Syntax.binder_bv - = x; - FStar_Syntax_Syntax.binder_qual - = uu___12; - FStar_Syntax_Syntax.binder_positivity - = uu___13; - FStar_Syntax_Syntax.binder_attrs - = uu___14;_}, - { - FStar_Syntax_Syntax.binder_bv - = y; - FStar_Syntax_Syntax.binder_qual - = uu___15; - FStar_Syntax_Syntax.binder_positivity - = uu___16; - FStar_Syntax_Syntax.binder_attrs - = uu___17;_}) - -> - let uu___18 = - let uu___19 = - FStar_Syntax_Syntax.bv_to_name - y in - (x, uu___19) in - FStar_Syntax_Syntax.NT - uu___18) - tbinders targs in - FStar_Syntax_Subst.subst s - tbody in - let env = - FStar_Compiler_List.fold_left - (fun env1 -> - fun uu___10 -> - match uu___10 with - | { - FStar_Syntax_Syntax.binder_bv - = a; - FStar_Syntax_Syntax.binder_qual - = uu___11; - FStar_Syntax_Syntax.binder_positivity - = uu___12; - FStar_Syntax_Syntax.binder_attrs - = uu___13;_} - -> - FStar_Extraction_ML_UEnv.extend_ty - env1 a false) g - targs in - let expected_t = - term_as_mlty env - expected_source_ty in - let polytype = - let uu___10 = - tbinders_as_ty_params env - targs in - (uu___10, expected_t) in - let add_unit = - match rest_args with - | [] -> - (let uu___10 = - is_fstar_value body1 in - Prims.op_Negation - uu___10) - || - (let uu___10 = - FStar_Syntax_Util.is_pure_comp - c1 in - Prims.op_Negation - uu___10) - | uu___10 -> false in - let rest_args1 = - if add_unit - then - let uu___10 = - unit_binder () in - uu___10 :: rest_args - else rest_args in - let polytype1 = - if add_unit - then - FStar_Extraction_ML_Syntax.push_unit - eff_body polytype - else polytype in - let body2 = - FStar_Syntax_Util.abs - rest_args1 body1 copt in - (lbname_, f_e, - (lbtyp1, (targs, polytype1)), - add_unit, has_c_inline, - body2)) - else - FStar_Compiler_Effect.failwith - "Not enough type binders") - | FStar_Syntax_Syntax.Tm_uinst uu___8 -> - let env = - FStar_Compiler_List.fold_left - (fun env1 -> - fun uu___9 -> - match uu___9 with - | { - FStar_Syntax_Syntax.binder_bv - = a; - FStar_Syntax_Syntax.binder_qual - = uu___10; - FStar_Syntax_Syntax.binder_positivity - = uu___11; - FStar_Syntax_Syntax.binder_attrs - = uu___12;_} - -> - FStar_Extraction_ML_UEnv.extend_ty - env1 a false) g tbinders in - let expected_t = term_as_mlty env tbody in - let polytype = - let uu___9 = - tbinders_as_ty_params env tbinders in - (uu___9, expected_t) in - let args = - FStar_Compiler_List.map - (fun uu___9 -> - match uu___9 with - | { - FStar_Syntax_Syntax.binder_bv = - bv; - FStar_Syntax_Syntax.binder_qual - = uu___10; - FStar_Syntax_Syntax.binder_positivity - = uu___11; - FStar_Syntax_Syntax.binder_attrs - = uu___12;_} - -> - let uu___13 = - FStar_Syntax_Syntax.bv_to_name - bv in - FStar_Syntax_Syntax.as_arg - uu___13) tbinders in - let e = - FStar_Syntax_Syntax.mk - (FStar_Syntax_Syntax.Tm_app - { - FStar_Syntax_Syntax.hd = lbdef1; - FStar_Syntax_Syntax.args = args - }) lbdef1.FStar_Syntax_Syntax.pos in - (lbname_, f_e, - (lbtyp1, (tbinders, polytype)), false, - has_c_inline, e) - | FStar_Syntax_Syntax.Tm_fvar uu___8 -> - let env = - FStar_Compiler_List.fold_left - (fun env1 -> - fun uu___9 -> - match uu___9 with - | { - FStar_Syntax_Syntax.binder_bv - = a; - FStar_Syntax_Syntax.binder_qual - = uu___10; - FStar_Syntax_Syntax.binder_positivity - = uu___11; - FStar_Syntax_Syntax.binder_attrs - = uu___12;_} - -> - FStar_Extraction_ML_UEnv.extend_ty - env1 a false) g tbinders in - let expected_t = term_as_mlty env tbody in - let polytype = - let uu___9 = - tbinders_as_ty_params env tbinders in - (uu___9, expected_t) in - let args = - FStar_Compiler_List.map - (fun uu___9 -> - match uu___9 with - | { - FStar_Syntax_Syntax.binder_bv = - bv; - FStar_Syntax_Syntax.binder_qual - = uu___10; - FStar_Syntax_Syntax.binder_positivity - = uu___11; - FStar_Syntax_Syntax.binder_attrs - = uu___12;_} - -> - let uu___13 = - FStar_Syntax_Syntax.bv_to_name - bv in - FStar_Syntax_Syntax.as_arg - uu___13) tbinders in - let e = - FStar_Syntax_Syntax.mk - (FStar_Syntax_Syntax.Tm_app - { - FStar_Syntax_Syntax.hd = lbdef1; - FStar_Syntax_Syntax.args = args - }) lbdef1.FStar_Syntax_Syntax.pos in - (lbname_, f_e, - (lbtyp1, (tbinders, polytype)), false, - has_c_inline, e) - | FStar_Syntax_Syntax.Tm_name uu___8 -> - let env = - FStar_Compiler_List.fold_left - (fun env1 -> - fun uu___9 -> - match uu___9 with - | { - FStar_Syntax_Syntax.binder_bv - = a; - FStar_Syntax_Syntax.binder_qual - = uu___10; - FStar_Syntax_Syntax.binder_positivity - = uu___11; - FStar_Syntax_Syntax.binder_attrs - = uu___12;_} - -> - FStar_Extraction_ML_UEnv.extend_ty - env1 a false) g tbinders in - let expected_t = term_as_mlty env tbody in - let polytype = - let uu___9 = - tbinders_as_ty_params env tbinders in - (uu___9, expected_t) in - let args = - FStar_Compiler_List.map - (fun uu___9 -> - match uu___9 with - | { - FStar_Syntax_Syntax.binder_bv = - bv; - FStar_Syntax_Syntax.binder_qual - = uu___10; - FStar_Syntax_Syntax.binder_positivity - = uu___11; - FStar_Syntax_Syntax.binder_attrs - = uu___12;_} - -> - let uu___13 = - FStar_Syntax_Syntax.bv_to_name - bv in - FStar_Syntax_Syntax.as_arg - uu___13) tbinders in - let e = - FStar_Syntax_Syntax.mk - (FStar_Syntax_Syntax.Tm_app - { - FStar_Syntax_Syntax.hd = lbdef1; - FStar_Syntax_Syntax.args = args - }) lbdef1.FStar_Syntax_Syntax.pos in - (lbname_, f_e, - (lbtyp1, (tbinders, polytype)), false, - has_c_inline, e) - | uu___8 -> err_value_restriction lbdef1)))) + FStar_Extraction_ML_UEnv.lookup_ty + env x in + uu___11.FStar_Extraction_ML_UEnv.ty_b_name in + let uu___11 = + FStar_Compiler_List.map + (fun attr -> + let uu___12 = + term_as_mlexpr g attr in + match uu___12 with + | (e, uu___13, uu___14) -> e) + binder_attrs in + { + FStar_Extraction_ML_Syntax.ty_param_name + = uu___10; + FStar_Extraction_ML_Syntax.ty_param_attrs + = uu___11 + }) in + (match lbdef1.FStar_Syntax_Syntax.n with + | FStar_Syntax_Syntax.Tm_abs + { FStar_Syntax_Syntax.bs = bs2; + FStar_Syntax_Syntax.body = body; + FStar_Syntax_Syntax.rc_opt = copt;_} + -> + let uu___7 = + FStar_Syntax_Subst.open_term bs2 body in + (match uu___7 with + | (bs3, body1) -> + if + n_tbinders <= + (FStar_Compiler_List.length bs3) + then + let uu___8 = + FStar_Compiler_Util.first_N + n_tbinders bs3 in + (match uu___8 with + | (targs, rest_args) -> + let expected_source_ty = + let s = + FStar_Compiler_List.map2 + (fun uu___9 -> + fun uu___10 -> + match (uu___9, + uu___10) + with + | ({ + FStar_Syntax_Syntax.binder_bv + = x; + FStar_Syntax_Syntax.binder_qual + = uu___11; + FStar_Syntax_Syntax.binder_positivity + = uu___12; + FStar_Syntax_Syntax.binder_attrs + = uu___13;_}, + { + FStar_Syntax_Syntax.binder_bv + = y; + FStar_Syntax_Syntax.binder_qual + = uu___14; + FStar_Syntax_Syntax.binder_positivity + = uu___15; + FStar_Syntax_Syntax.binder_attrs + = uu___16;_}) + -> + let uu___17 = + let uu___18 = + FStar_Syntax_Syntax.bv_to_name + y in + (x, uu___18) in + FStar_Syntax_Syntax.NT + uu___17) + tbinders targs in + FStar_Syntax_Subst.subst s + tbody in + let env = + FStar_Compiler_List.fold_left + (fun env1 -> + fun uu___9 -> + match uu___9 with + | { + FStar_Syntax_Syntax.binder_bv + = a; + FStar_Syntax_Syntax.binder_qual + = uu___10; + FStar_Syntax_Syntax.binder_positivity + = uu___11; + FStar_Syntax_Syntax.binder_attrs + = uu___12;_} + -> + FStar_Extraction_ML_UEnv.extend_ty + env1 a false) g + targs in + let expected_t = + term_as_mlty env + expected_source_ty in + let polytype = + let uu___9 = + tbinders_as_ty_params env + targs in + (uu___9, expected_t) in + let add_unit = + match rest_args with + | [] -> + (let uu___9 = + is_fstar_value body1 in + Prims.op_Negation uu___9) + || + (let uu___9 = + FStar_Syntax_Util.is_pure_comp + c1 in + Prims.op_Negation + uu___9) + | uu___9 -> false in + let rest_args1 = + if add_unit + then + let uu___9 = unit_binder () in + uu___9 :: rest_args + else rest_args in + let polytype1 = + if add_unit + then + FStar_Extraction_ML_Syntax.push_unit + eff_body polytype + else polytype in + let body2 = + FStar_Syntax_Util.abs + rest_args1 body1 copt in + (lbname_, f_e, + (lbtyp1, (targs, polytype1)), + add_unit, has_c_inline, + body2)) + else + FStar_Compiler_Effect.failwith + "Not enough type binders") + | FStar_Syntax_Syntax.Tm_uinst uu___7 -> + let env = + FStar_Compiler_List.fold_left + (fun env1 -> + fun uu___8 -> + match uu___8 with + | { + FStar_Syntax_Syntax.binder_bv + = a; + FStar_Syntax_Syntax.binder_qual + = uu___9; + FStar_Syntax_Syntax.binder_positivity + = uu___10; + FStar_Syntax_Syntax.binder_attrs + = uu___11;_} + -> + FStar_Extraction_ML_UEnv.extend_ty + env1 a false) g tbinders in + let expected_t = term_as_mlty env tbody in + let polytype = + let uu___8 = + tbinders_as_ty_params env tbinders in + (uu___8, expected_t) in + let args = + FStar_Compiler_List.map + (fun uu___8 -> + match uu___8 with + | { + FStar_Syntax_Syntax.binder_bv = + bv; + FStar_Syntax_Syntax.binder_qual + = uu___9; + FStar_Syntax_Syntax.binder_positivity + = uu___10; + FStar_Syntax_Syntax.binder_attrs + = uu___11;_} + -> + let uu___12 = + FStar_Syntax_Syntax.bv_to_name + bv in + FStar_Syntax_Syntax.as_arg + uu___12) tbinders in + let e = + FStar_Syntax_Syntax.mk + (FStar_Syntax_Syntax.Tm_app + { + FStar_Syntax_Syntax.hd = lbdef1; + FStar_Syntax_Syntax.args = args + }) lbdef1.FStar_Syntax_Syntax.pos in + (lbname_, f_e, + (lbtyp1, (tbinders, polytype)), false, + has_c_inline, e) + | FStar_Syntax_Syntax.Tm_fvar uu___7 -> + let env = + FStar_Compiler_List.fold_left + (fun env1 -> + fun uu___8 -> + match uu___8 with + | { + FStar_Syntax_Syntax.binder_bv + = a; + FStar_Syntax_Syntax.binder_qual + = uu___9; + FStar_Syntax_Syntax.binder_positivity + = uu___10; + FStar_Syntax_Syntax.binder_attrs + = uu___11;_} + -> + FStar_Extraction_ML_UEnv.extend_ty + env1 a false) g tbinders in + let expected_t = term_as_mlty env tbody in + let polytype = + let uu___8 = + tbinders_as_ty_params env tbinders in + (uu___8, expected_t) in + let args = + FStar_Compiler_List.map + (fun uu___8 -> + match uu___8 with + | { + FStar_Syntax_Syntax.binder_bv = + bv; + FStar_Syntax_Syntax.binder_qual + = uu___9; + FStar_Syntax_Syntax.binder_positivity + = uu___10; + FStar_Syntax_Syntax.binder_attrs + = uu___11;_} + -> + let uu___12 = + FStar_Syntax_Syntax.bv_to_name + bv in + FStar_Syntax_Syntax.as_arg + uu___12) tbinders in + let e = + FStar_Syntax_Syntax.mk + (FStar_Syntax_Syntax.Tm_app + { + FStar_Syntax_Syntax.hd = lbdef1; + FStar_Syntax_Syntax.args = args + }) lbdef1.FStar_Syntax_Syntax.pos in + (lbname_, f_e, + (lbtyp1, (tbinders, polytype)), false, + has_c_inline, e) + | FStar_Syntax_Syntax.Tm_name uu___7 -> + let env = + FStar_Compiler_List.fold_left + (fun env1 -> + fun uu___8 -> + match uu___8 with + | { + FStar_Syntax_Syntax.binder_bv + = a; + FStar_Syntax_Syntax.binder_qual + = uu___9; + FStar_Syntax_Syntax.binder_positivity + = uu___10; + FStar_Syntax_Syntax.binder_attrs + = uu___11;_} + -> + FStar_Extraction_ML_UEnv.extend_ty + env1 a false) g tbinders in + let expected_t = term_as_mlty env tbody in + let polytype = + let uu___8 = + tbinders_as_ty_params env tbinders in + (uu___8, expected_t) in + let args = + FStar_Compiler_List.map + (fun uu___8 -> + match uu___8 with + | { + FStar_Syntax_Syntax.binder_bv = + bv; + FStar_Syntax_Syntax.binder_qual + = uu___9; + FStar_Syntax_Syntax.binder_positivity + = uu___10; + FStar_Syntax_Syntax.binder_attrs + = uu___11;_} + -> + let uu___12 = + FStar_Syntax_Syntax.bv_to_name + bv in + FStar_Syntax_Syntax.as_arg + uu___12) tbinders in + let e = + FStar_Syntax_Syntax.mk + (FStar_Syntax_Syntax.Tm_app + { + FStar_Syntax_Syntax.hd = lbdef1; + FStar_Syntax_Syntax.args = args + }) lbdef1.FStar_Syntax_Syntax.pos in + (lbname_, f_e, + (lbtyp1, (tbinders, polytype)), false, + has_c_inline, e) + | uu___7 -> err_value_restriction lbdef1))) | uu___5 -> no_gen ()) in FStar_Compiler_List.map maybe_generalize (FStar_Pervasives_Native.snd lbs) @@ -3115,13 +3106,11 @@ and (term_as_mlexpr' : FStar_Class_Show.show FStar_Syntax_Print.showable_fv fv in let uu___9 = - let uu___10 = - FStar_Extraction_ML_UEnv.current_module_of_uenv g in - FStar_Extraction_ML_Code.string_of_mlexpr uu___10 x in + FStar_Class_Show.show + FStar_Extraction_ML_Code.showable_mlexpr x in let uu___10 = - let uu___11 = - FStar_Extraction_ML_UEnv.current_module_of_uenv g in - FStar_Extraction_ML_Code.string_of_mlty uu___11 + FStar_Class_Show.show + FStar_Extraction_ML_Code.showable_mlty (FStar_Pervasives_Native.snd mltys) in FStar_Compiler_Util.print3 "looked up %s: got %s at %s \n" uu___8 uu___9 @@ -3559,18 +3548,12 @@ and (term_as_mlexpr' : FStar_Class_Show.show FStar_Syntax_Print.showable_term head1 in let uu___10 = - let uu___11 = - FStar_Extraction_ML_UEnv.current_module_of_uenv - g in - FStar_Extraction_ML_Code.string_of_mlexpr - uu___11 + FStar_Class_Show.show + FStar_Extraction_ML_Code.showable_mlexpr exp_b.FStar_Extraction_ML_UEnv.exp_b_expr in let uu___11 = - let uu___12 = - FStar_Extraction_ML_UEnv.current_module_of_uenv - g in - FStar_Extraction_ML_Code.string_of_mlty - uu___12 + FStar_Class_Show.show + FStar_Extraction_ML_Code.showable_mlty (FStar_Pervasives_Native.snd exp_b.FStar_Extraction_ML_UEnv.exp_b_tscheme) in let uu___12 = @@ -3691,18 +3674,12 @@ and (term_as_mlexpr' : FStar_Class_Show.show FStar_Syntax_Print.showable_term head1 in let uu___10 = - let uu___11 = - FStar_Extraction_ML_UEnv.current_module_of_uenv - g in - FStar_Extraction_ML_Code.string_of_mlexpr - uu___11 + FStar_Class_Show.show + FStar_Extraction_ML_Code.showable_mlexpr exp_b.FStar_Extraction_ML_UEnv.exp_b_expr in let uu___11 = - let uu___12 = - FStar_Extraction_ML_UEnv.current_module_of_uenv - g in - FStar_Extraction_ML_Code.string_of_mlty - uu___12 + FStar_Class_Show.show + FStar_Extraction_ML_Code.showable_mlty (FStar_Pervasives_Native.snd exp_b.FStar_Extraction_ML_UEnv.exp_b_tscheme) in let uu___12 = @@ -4145,69 +4122,55 @@ and (term_as_mlexpr' : | (nm, (_lbname, f, (_t, (targs, polytype)), add_unit, has_c_inline, e)) -> - (FStar_Extraction_ML_UEnv.debug g - (fun uu___4 -> - let uu___5 = - FStar_Class_Show.show - (FStar_Class_Show.printableshow - FStar_Class_Printable.printable_string) nm in - let uu___6 = - FStar_Class_Show.show - FStar_Extraction_ML_Code.showable_mlty - (FStar_Pervasives_Native.snd polytype) in - FStar_Compiler_Util.print2 - "Checking lb %s at %s\n" uu___5 uu___6); - (let env1 = - FStar_Compiler_List.fold_left - (fun env2 -> - fun uu___4 -> - match uu___4 with - | { FStar_Syntax_Syntax.binder_bv = a; - FStar_Syntax_Syntax.binder_qual = uu___5; - FStar_Syntax_Syntax.binder_positivity = - uu___6; - FStar_Syntax_Syntax.binder_attrs = - uu___7;_} - -> - FStar_Extraction_ML_UEnv.extend_ty env2 - a false) env targs in - let expected_t = FStar_Pervasives_Native.snd polytype in - let uu___4 = check_term_as_mlexpr env1 e f expected_t in - match uu___4 with - | (e1, ty) -> - let uu___5 = maybe_promote_effect e1 f expected_t in - (match uu___5 with - | (e2, f1) -> - let meta = - match (f1, ty) with - | (FStar_Extraction_ML_Syntax.E_PURE, - FStar_Extraction_ML_Syntax.MLTY_Erased) - -> [FStar_Extraction_ML_Syntax.Erased] - | (FStar_Extraction_ML_Syntax.E_ERASABLE, - FStar_Extraction_ML_Syntax.MLTY_Erased) - -> [FStar_Extraction_ML_Syntax.Erased] - | uu___6 -> [] in - let meta1 = - if has_c_inline - then FStar_Extraction_ML_Syntax.CInline :: - meta - else meta in - (f1, - { - FStar_Extraction_ML_Syntax.mllb_name = - nm; - FStar_Extraction_ML_Syntax.mllb_tysc = - (FStar_Pervasives_Native.Some polytype); - FStar_Extraction_ML_Syntax.mllb_add_unit - = add_unit; - FStar_Extraction_ML_Syntax.mllb_def = e2; - FStar_Extraction_ML_Syntax.mllb_attrs = - []; - FStar_Extraction_ML_Syntax.mllb_meta = - meta1; - FStar_Extraction_ML_Syntax.print_typ = - true - })))) in + let env1 = + FStar_Compiler_List.fold_left + (fun env2 -> + fun uu___3 -> + match uu___3 with + | { FStar_Syntax_Syntax.binder_bv = a; + FStar_Syntax_Syntax.binder_qual = uu___4; + FStar_Syntax_Syntax.binder_positivity = + uu___5; + FStar_Syntax_Syntax.binder_attrs = uu___6;_} + -> + FStar_Extraction_ML_UEnv.extend_ty env2 a + false) env targs in + let expected_t = FStar_Pervasives_Native.snd polytype in + let uu___3 = check_term_as_mlexpr env1 e f expected_t in + (match uu___3 with + | (e1, ty) -> + let uu___4 = maybe_promote_effect e1 f expected_t in + (match uu___4 with + | (e2, f1) -> + let meta = + match (f1, ty) with + | (FStar_Extraction_ML_Syntax.E_PURE, + FStar_Extraction_ML_Syntax.MLTY_Erased) + -> [FStar_Extraction_ML_Syntax.Erased] + | (FStar_Extraction_ML_Syntax.E_ERASABLE, + FStar_Extraction_ML_Syntax.MLTY_Erased) + -> [FStar_Extraction_ML_Syntax.Erased] + | uu___5 -> [] in + let meta1 = + if has_c_inline + then FStar_Extraction_ML_Syntax.CInline :: + meta + else meta in + (f1, + { + FStar_Extraction_ML_Syntax.mllb_name = nm; + FStar_Extraction_ML_Syntax.mllb_tysc = + (FStar_Pervasives_Native.Some polytype); + FStar_Extraction_ML_Syntax.mllb_add_unit + = add_unit; + FStar_Extraction_ML_Syntax.mllb_def = e2; + FStar_Extraction_ML_Syntax.mllb_attrs = + []; + FStar_Extraction_ML_Syntax.mllb_meta = + meta1; + FStar_Extraction_ML_Syntax.print_typ = + true + }))) in let lbs3 = extract_lb_sig g (is_rec, lbs2) in let uu___2 = FStar_Compiler_List.fold_right diff --git a/src/extraction/FStar.Extraction.ML.Code.fst b/src/extraction/FStar.Extraction.ML.Code.fst index 69b9914b416..5b879ad77d4 100644 --- a/src/extraction/FStar.Extraction.ML.Code.fst +++ b/src/extraction/FStar.Extraction.ML.Code.fst @@ -352,7 +352,7 @@ let rec doc_of_mltype' (currentModule : mlsymbol) (outer : level) (ty : mlty) = | MLTY_Fun (t1, et, t2) -> let d1 = doc_of_mltype currentModule (t_prio_fun, Left ) t1 in let d2 = doc_of_mltype currentModule (t_prio_fun, Right) t2 in - maybe_paren outer t_prio_fun (hbox (reduce1 [d1; text "->"; d2])) + maybe_paren outer t_prio_fun (hbox (reduce1 [d1; text " -> "; d2])) | MLTY_Top -> if Util.codegen_fsharp() diff --git a/src/extraction/FStar.Extraction.ML.Term.fst b/src/extraction/FStar.Extraction.ML.Term.fst index ed39e93a955..9e481e2423f 100644 --- a/src/extraction/FStar.Extraction.ML.Term.fst +++ b/src/extraction/FStar.Extraction.ML.Term.fst @@ -1244,16 +1244,18 @@ let rec extract_lb_sig (g:uenv) (lbs:letbindings) : list lb_sig = //If, after erasure, what remains is not a value, then add an extra unit arg. to preserve order of evaluation/generativity //and to circumvent the value restriction - //TODO: ERASE ONLY THOSE THAT ABSTRACT OVER PURE FUNCTIONS in Type(i), - // NOT, e.g., (x:int -> St Type) + //We also erase type arguments that abstract over impure functions, + //replacing the type arguments with a single unit. + //For example, `a:Type -> Dv a` is extracted to `unit -Impure-> 'a` + //The important thing is that we retain an effect tag on the arrow to note + //that the type application is impure. + //See Issue #3473 let etag_of_comp c = effect_as_etag g (U.comp_effect_name c) in let tbinders, eff_body, tbody = match BU.prefix_until (fun x -> not (is_type_binder g x)) bs with | None -> bs, etag_of_comp c, U.comp_result c | Some (bs, b, rest) -> bs, E_PURE, U.arrow (b::rest) c in - debug g (fun () -> - BU.print1 "Extract LB SIG: %s\n" (show tbody)); let n_tbinders = List.length tbinders in let lbdef = normalize_abs lbdef |> U.unmeta in let tbinders_as_ty_params env = List.map (fun ({binder_bv=x; binder_attrs}) -> { @@ -1277,7 +1279,12 @@ let rec extract_lb_sig (g:uenv) (lbs:letbindings) : list lb_sig = || not (U.is_pure_comp c) | _ -> false in let rest_args = if add_unit then (unit_binder()::rest_args) else rest_args in - let polytype = if add_unit then push_unit eff_body polytype else polytype in + let polytype = + if add_unit + then (* record the effect of type application, eff_body *) + push_unit eff_body polytype + else polytype + in let body = U.abs rest_args body copt in (lbname_, f_e, (lbtyp, (targs, polytype)), add_unit, has_c_inline, body) @@ -1521,7 +1528,9 @@ and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr & e_tag & mlty) = ml_unit, E_PURE, ml_unit_ty | Inr ({exp_b_expr=x; exp_b_tscheme=mltys; exp_b_eff=etag}), qual -> - //let _ = printfn "\n (*looked up tyscheme of \n %A \n as \n %A *) \n" x s in + //etag is the effect associated with simply using t, since it may + //be an effectful type application in F* + //in the common case, etag is E_PURE begin match mltys with | ([], t) when t=ml_unit_ty -> ml_unit, etag, t //optimize (x:unit) to () @@ -1551,8 +1560,8 @@ and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr & e_tag & mlty) = let _ = debug g (fun () -> BU.print3 "looked up %s: got %s at %s \n" (show fv) - (Code.string_of_mlexpr (current_module_of_uenv g) x) - (Code.string_of_mlty (current_module_of_uenv g) (snd mltys))) in + (show x) + (show (snd mltys))) in begin match mltys with | ([], t) when (t=ml_unit_ty) -> ml_unit, E_PURE, t //optimize (x:unit) to () | ([], t) -> maybe_eta_data_and_project_record g fv.fv_qual t x, E_PURE, t @@ -1730,8 +1739,8 @@ and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr & e_tag & mlty) = debug g (fun () -> BU.print4 "@@@looked up %s: got %s at %s with eff <%s>\n" (show head) - (Code.string_of_mlexpr (current_module_of_uenv g) exp_b.exp_b_expr) - (Code.string_of_mlty (current_module_of_uenv g) (snd exp_b.exp_b_tscheme)) + (show exp_b.exp_b_expr) + (show (snd exp_b.exp_b_tscheme)) (show exp_b.exp_b_eff)); (exp_b.exp_b_expr, exp_b.exp_b_tscheme, exp_b.exp_b_eff), q | _ -> failwith "FIXME Ty" in @@ -1931,7 +1940,6 @@ and term_as_mlexpr' (g:uenv) (top:term) : (mlexpr & e_tag & mlty) = let check_lb env (nm_sig : mlident & lb_sig) = let (nm, (_lbname, f, (_t, (targs, polytype)), add_unit, has_c_inline, e)) = nm_sig in - debug g (fun () -> BU.print2 "Checking lb %s at %s\n" (show nm) (show (snd polytype))); let env = List.fold_left (fun env ({binder_bv=a}) -> UEnv.extend_ty env a false) env targs in let expected_t = snd polytype in let e, ty = check_term_as_mlexpr env e f expected_t in